Theorem mpan2d 419

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 254	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpid 41	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  mpand  420  mpan2i  422  ralxfrd  4284  rexxfrd  4285  elunirn  5545  onunsnss  6625  xpfi  6638  snon0  6643  genprndl  7078  genprndu  7079  addlsub  7846  letrp1  8307  peano2uz2  8851  uzind  8855  xrre  9280  xrre2  9281  flqge  9685  monoord  9900  facwordi  10144  facavg  10150  dvdsmultr1  11108  ltoddhalfle  11167  dvdsgcdb  11276  dfgcd2  11277  coprmgcdb  11344  coprmdvds2  11349  exprmfct  11393  prmdvdsfz  11394  prmfac1  11405  rpexp  11406