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  4494  rexxfrd  4495  elunirn  5810  onunsnss  6975  xpfi  6988  snon0  6996  genprndl  7583  genprndu  7584  addlsub  8391  letrp1  8869  peano2uz2  9427  uzind  9431  xrre  9889  xrre2  9890  flqge  10354  monoord  10559  facwordi  10814  facavg  10820  dvdsmultr1  11977  ltoddhalfle  12037  dvdsgcdb  12153  dfgcd2  12154  coprmgcdb  12229  coprmdvds2  12234  exprmfct  12279  prmdvdsfz  12280  prmfac1  12293  rpexp  12294  eulerthlemh  12372  pcpremul  12434  pcdvdsb  12461  pcprmpw2  12474  pockthlem  12497  4sqlem11  12542  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad2lem2  15239