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  4588  rexxfrd  4589  elunirn  5945  onunsnss  7190  xpfi  7205  snon0  7215  genprndl  7852  genprndu  7853  addlsub  8659  letrp1  9139  peano2uz2  9703  uzind  9707  xrre  10172  xrre2  10173  flqge  10666  monoord  10871  facwordi  11127  facavg  11133  dvdsmultr1  12542  ltoddhalfle  12604  dvdsgcdb  12734  dfgcd2  12735  coprmgcdb  12810  coprmdvds2  12815  exprmfct  12860  prmdvdsfz  12861  prmfac1  12874  rpexp  12875  eulerthlemh  12953  pcpremul  13016  pcdvdsb  13043  pcprmpw2  13056  pockthlem  13079  4sqlem11  13124  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem1  16080  lgsquad2lem2  16081