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  7888  genprndu  7889  addlsub  8696  letrp1  9178  peano2uz2  9753  uzind  9757  xrre  10222  xrre2  10223  flqge  10717  monoord  10922  facwordi  11178  facavg  11184  dvdsmultr1  12598  ltoddhalfle  12660  dvdsgcdb  12790  dfgcd2  12791  coprmgcdb  12866  coprmdvds2  12871  exprmfct  12916  prmdvdsfz  12917  prmfac1  12930  rpexp  12931  eulerthlemh  13009  pcpremul  13072  pcdvdsb  13099  pcprmpw2  13112  pockthlem  13135  4sqlem11  13180  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  lgsquad2lem2  16201