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  4509  rexxfrd  4510  elunirn  5835  onunsnss  7014  xpfi  7029  snon0  7037  genprndl  7634  genprndu  7635  addlsub  8442  letrp1  8921  peano2uz2  9480  uzind  9484  xrre  9942  xrre2  9943  flqge  10425  monoord  10630  facwordi  10885  facavg  10891  dvdsmultr1  12142  ltoddhalfle  12204  dvdsgcdb  12334  dfgcd2  12335  coprmgcdb  12410  coprmdvds2  12415  exprmfct  12460  prmdvdsfz  12461  prmfac1  12474  rpexp  12475  eulerthlemh  12553  pcpremul  12616  pcdvdsb  12643  pcprmpw2  12656  pockthlem  12679  4sqlem11  12724  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  lgseisenlem1  15547  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad2lem2  15559