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  4498  rexxfrd  4499  elunirn  5816  onunsnss  6987  xpfi  7002  snon0  7010  genprndl  7605  genprndu  7606  addlsub  8413  letrp1  8892  peano2uz2  9450  uzind  9454  xrre  9912  xrre2  9913  flqge  10389  monoord  10594  facwordi  10849  facavg  10855  dvdsmultr1  12013  ltoddhalfle  12075  dvdsgcdb  12205  dfgcd2  12206  coprmgcdb  12281  coprmdvds2  12286  exprmfct  12331  prmdvdsfz  12332  prmfac1  12345  rpexp  12346  eulerthlemh  12424  pcpremul  12487  pcdvdsb  12514  pcprmpw2  12527  pockthlem  12550  4sqlem11  12595  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem1  15406  lgsquad2lem2  15407