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  4608  rexxfrd  4609  elunirn  5972  onunsnss  7224  xpfi  7239  snon0  7249  genprndl  7889  genprndu  7890  addlsub  8698  letrp1  9181  peano2uz2  9758  uzind  9762  xrre  10233  xrre2  10234  flqge  10730  flapge  10731  monoord  10937  facwordi  11194  facavg  11200  dvdsmultr1  12617  ltoddhalfle  12679  dvdsgcdb  12809  dfgcd2  12810  coprmgcdb  12885  coprmdvds2  12890  exprmfct  12936  prmdvdsfz  12937  prmfac1  12950  rpexp  12951  eulerthlemh  13032  pcpremul  13095  pcdvdsb  13122  pcprmpw2  13135  pockthlem  13158  4sqlem11  13203  chtqub  16270  bposlem3  16287  lgsne0  16336  gausslemma2dlem1a  16356  gausslemma2dlem2  16360  lgseisenlem1  16368  lgseisenlem2  16369  lgsquadlem1  16375  lgsquadlem2  16376  lgsquadlem3  16377  lgsquad2lem1  16379  lgsquad2lem2  16380