Theorem mpd3an3 917

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpd3an3.2	|- ((ph /\ ps) -> ch)
mpd3an3.3	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mpd3an3	|- ((ph /\ ps) -> th)

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 |- ((ph /\ ps) -> ch)
2		mpd3an3.3	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expa 833	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpdan 704	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  cdavalt 4919  fzrevral3t 6521  subsq2t 6643  cncfval 7264  cnpfval 7757  lmconst 7934  nvge0 8302  nvnd 8319  ip0r 8370  ip0l 8371  nmo0 8451  spwval2 8653  hi2eqt 8971  elghomlem1 10382  symgoprval 10404  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain