Theorem mpan2d 425

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpand  426  mpan2i  428  ralxfrd  4439  rexxfrd  4440  elunirn  5733  onunsnss  6878  xpfi  6891  snon0  6897  genprndl  7458  genprndu  7459  addlsub  8264  letrp1  8739  peano2uz2  9294  uzind  9298  xrre  9752  xrre2  9753  flqge  10213  monoord  10407  facwordi  10649  facavg  10655  dvdsmultr1  11767  ltoddhalfle  11826  dvdsgcdb  11942  dfgcd2  11943  coprmgcdb  12016  coprmdvds2  12021  exprmfct  12066  prmdvdsfz  12067  prmfac1  12080  rpexp  12081  eulerthlemh  12159  pcpremul  12221  pcdvdsb  12247  pcprmpw2  12260  pockthlem  12282  lgsne0  13539