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  4391  rexxfrd  4392  elunirn  5675  onunsnss  6813  xpfi  6826  snon0  6832  genprndl  7353  genprndu  7354  addlsub  8156  letrp1  8630  peano2uz2  9182  uzind  9186  xrre  9633  xrre2  9634  flqge  10086  monoord  10280  facwordi  10518  facavg  10524  dvdsmultr1  11567  ltoddhalfle  11626  dvdsgcdb  11737  dfgcd2  11738  coprmgcdb  11805  coprmdvds2  11810  exprmfct  11854  prmdvdsfz  11855  prmfac1  11866  rpexp  11867