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  4497  rexxfrd  4498  elunirn  5813  onunsnss  6978  xpfi  6993  snon0  7001  genprndl  7588  genprndu  7589  addlsub  8396  letrp1  8875  peano2uz2  9433  uzind  9437  xrre  9895  xrre2  9896  flqge  10372  monoord  10577  facwordi  10832  facavg  10838  dvdsmultr1  11996  ltoddhalfle  12058  dvdsgcdb  12180  dfgcd2  12181  coprmgcdb  12256  coprmdvds2  12261  exprmfct  12306  prmdvdsfz  12307  prmfac1  12320  rpexp  12321  eulerthlemh  12399  pcpremul  12462  pcdvdsb  12489  pcprmpw2  12502  pockthlem  12525  4sqlem11  12570  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad2lem2  15323