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  7230  xpfi  7245  snon0  7255  genprndl  7894  genprndu  7895  addlsub  8703  letrp1  9186  peano2uz2  9763  uzind  9767  xrre  10238  xrre2  10239  flqge  10735  flapge  10736  monoord  10942  facwordi  11199  facavg  11205  dvdsmultr1  12622  ltoddhalfle  12684  dvdsgcdb  12814  dfgcd2  12815  coprmgcdb  12890  coprmdvds2  12895  exprmfct  12941  prmdvdsfz  12942  prmfac1  12955  rpexp  12956  eulerthlemh  13037  pcpremul  13100  pcdvdsb  13127  pcprmpw2  13140  pockthlem  13163  4sqlem11  13208  chtqub  16313  bposlem3  16330  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  lgseisenlem1  16411  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  lgsquad2lem2  16423