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  4555  rexxfrd  4556  elunirn  5900  onunsnss  7100  xpfi  7115  snon0  7123  genprndl  7729  genprndu  7730  addlsub  8537  letrp1  9016  peano2uz2  9575  uzind  9579  xrre  10043  xrre2  10044  flqge  10530  monoord  10735  facwordi  10990  facavg  10996  dvdsmultr1  12379  ltoddhalfle  12441  dvdsgcdb  12571  dfgcd2  12572  coprmgcdb  12647  coprmdvds2  12652  exprmfct  12697  prmdvdsfz  12698  prmfac1  12711  rpexp  12712  eulerthlemh  12790  pcpremul  12853  pcdvdsb  12880  pcprmpw2  12893  pockthlem  12916  4sqlem11  12961  lgsne0  15754  gausslemma2dlem1a  15774  gausslemma2dlem2  15778  lgseisenlem1  15786  lgseisenlem2  15787  lgsquadlem1  15793  lgsquadlem2  15794  lgsquadlem3  15795  lgsquad2lem1  15797  lgsquad2lem2  15798