Theorem mpan2d 418

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  419  mpan2i  421  ralxfrd  4212  rexxfrd  4213  elunirn  5426  onunsnss  6383  snon0  6387  genprndl  6711  genprndu  6712  addlsub  7474  letrp1  7926  peano2uz2  8454  uzind  8458  xrre  8887  xrre2  8888  flqge  9284  monoord  9455  facwordi  9667  facavg  9673  dvdsmultr1  10233  ltoddhalfle  10293  dvdsgcdb  10402  dfgcd2  10403  coprmgcdb  10470  coprmdvds2  10475  exprmfct  10519  prmdvdsfz  10520  prmfac1  10531  rpexp  10532