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  4552  rexxfrd  4553  elunirn  5889  onunsnss  7075  xpfi  7090  snon0  7098  genprndl  7704  genprndu  7705  addlsub  8512  letrp1  8991  peano2uz2  9550  uzind  9554  xrre  10012  xrre2  10013  flqge  10497  monoord  10702  facwordi  10957  facavg  10963  dvdsmultr1  12337  ltoddhalfle  12399  dvdsgcdb  12529  dfgcd2  12530  coprmgcdb  12605  coprmdvds2  12610  exprmfct  12655  prmdvdsfz  12656  prmfac1  12669  rpexp  12670  eulerthlemh  12748  pcpremul  12811  pcdvdsb  12838  pcprmpw2  12851  pockthlem  12874  4sqlem11  12919  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  lgseisenlem1  15743  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  lgsquad2lem2  15755