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  4565  rexxfrd  4566  elunirn  5917  onunsnss  7152  xpfi  7167  snon0  7177  genprndl  7784  genprndu  7785  addlsub  8591  letrp1  9070  peano2uz2  9631  uzind  9635  xrre  10099  xrre2  10100  flqge  10588  monoord  10793  facwordi  11048  facavg  11054  dvdsmultr1  12455  ltoddhalfle  12517  dvdsgcdb  12647  dfgcd2  12648  coprmgcdb  12723  coprmdvds2  12728  exprmfct  12773  prmdvdsfz  12774  prmfac1  12787  rpexp  12788  eulerthlemh  12866  pcpremul  12929  pcdvdsb  12956  pcprmpw2  12969  pockthlem  12992  4sqlem11  13037  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  lgseisenlem1  15872  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  lgsquad2lem2  15884