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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpand  433  mpan2i  435  ralxfrd  4610  rexxfrd  4611  elunirn  5975  onunsnss  7228  xpfi  7243  snon0  7253  genprndl  7894  genprndu  7895  addlsub  8703  letrp1  9186  peano2uz2  9764  uzind  9768  xrre  10239  xrre2  10240  flqge  10736  flapge  10737  monoord  10943  facwordi  11200  facavg  11206  dvdsmultr1  12623  ltoddhalfle  12685  dvdsgcdb  12815  dfgcd2  12816  coprmgcdb  12891  coprmdvds2  12896  exprmfct  12942  prmdvdsfz  12943  prmfac1  12956  rpexp  12957  eulerthlemh  13038  pcpremul  13101  pcdvdsb  13128  pcprmpw2  13141  pockthlem  13164  4sqlem11  13209  chtqub  16296  bposlem3  16313  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  lgseisenlem1  16394  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  lgsquad2lem2  16406