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  4583  rexxfrd  4584  elunirn  5939  onunsnss  7177  xpfi  7192  snon0  7202  genprndl  7836  genprndu  7837  addlsub  8643  letrp1  9122  peano2uz2  9685  uzind  9689  xrre  10153  xrre2  10154  flqge  10642  monoord  10847  facwordi  11102  facavg  11108  dvdsmultr1  12517  ltoddhalfle  12579  dvdsgcdb  12709  dfgcd2  12710  coprmgcdb  12785  coprmdvds2  12790  exprmfct  12835  prmdvdsfz  12836  prmfac1  12849  rpexp  12850  eulerthlemh  12928  pcpremul  12991  pcdvdsb  13018  pcprmpw2  13031  pockthlem  13054  4sqlem11  13099  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  lgseisenlem1  15943  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad2lem2  15955