Theorem mpan2d 428

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  429  mpan2i  431  ralxfrd  4508  rexxfrd  4509  elunirn  5834  onunsnss  7013  xpfi  7028  snon0  7036  genprndl  7633  genprndu  7634  addlsub  8441  letrp1  8920  peano2uz2  9479  uzind  9483  xrre  9941  xrre2  9942  flqge  10423  monoord  10628  facwordi  10883  facavg  10889  dvdsmultr1  12113  ltoddhalfle  12175  dvdsgcdb  12305  dfgcd2  12306  coprmgcdb  12381  coprmdvds2  12386  exprmfct  12431  prmdvdsfz  12432  prmfac1  12445  rpexp  12446  eulerthlemh  12524  pcpremul  12587  pcdvdsb  12614  pcprmpw2  12627  pockthlem  12650  4sqlem11  12695  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  lgsquad2lem2  15530