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  4559  rexxfrd  4560  elunirn  5906  onunsnss  7108  xpfi  7123  snon0  7133  genprndl  7740  genprndu  7741  addlsub  8548  letrp1  9027  peano2uz2  9586  uzind  9590  xrre  10054  xrre2  10055  flqge  10541  monoord  10746  facwordi  11001  facavg  11007  dvdsmultr1  12391  ltoddhalfle  12453  dvdsgcdb  12583  dfgcd2  12584  coprmgcdb  12659  coprmdvds2  12664  exprmfct  12709  prmdvdsfz  12710  prmfac1  12723  rpexp  12724  eulerthlemh  12802  pcpremul  12865  pcdvdsb  12892  pcprmpw2  12905  pockthlem  12928  4sqlem11  12973  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  lgsquad2lem2  15810