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  4557  rexxfrd  4558  elunirn  5902  onunsnss  7102  xpfi  7117  snon0  7125  genprndl  7731  genprndu  7732  addlsub  8539  letrp1  9018  peano2uz2  9577  uzind  9581  xrre  10045  xrre2  10046  flqge  10532  monoord  10737  facwordi  10992  facavg  10998  dvdsmultr1  12382  ltoddhalfle  12444  dvdsgcdb  12574  dfgcd2  12575  coprmgcdb  12650  coprmdvds2  12655  exprmfct  12700  prmdvdsfz  12701  prmfac1  12714  rpexp  12715  eulerthlemh  12793  pcpremul  12856  pcdvdsb  12883  pcprmpw2  12896  pockthlem  12919  4sqlem11  12964  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad2lem2  15801