Theorem mpan2d 432

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mpan2d.1	|- ( ph -> ch )
mpan2d.2	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
mpan2d	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpan2d

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 |- ( ph -> ch )
2		mpan2d.2	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 258	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpid 42	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpand  433  mpan2i  435  ralxfrd  4603  rexxfrd  4604  elunirn  5962  onunsnss  7214  xpfi  7229  snon0  7239  genprndl  7878  genprndu  7879  addlsub  8686  letrp1  9168  peano2uz2  9732  uzind  9736  xrre  10201  xrre2  10202  flqge  10695  monoord  10900  facwordi  11156  facavg  11162  dvdsmultr1  12576  ltoddhalfle  12638  dvdsgcdb  12768  dfgcd2  12769  coprmgcdb  12844  coprmdvds2  12849  exprmfct  12894  prmdvdsfz  12895  prmfac1  12908  rpexp  12909  eulerthlemh  12987  pcpremul  13050  pcdvdsb  13077  pcprmpw2  13090  pockthlem  13113  4sqlem11  13158  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  lgsquad2lem2  16115