Theorem mpan2d 404

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

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  mpand  405  mpan2i  407  ralxfrd  4194  rexxfrd  4195  elunirn  5405  onunsnss  6355  snon0  6356  genprndl  6619  genprndu  6620  letrp1  7814  peano2uz2  8345  uzind  8349  xrre  8733  xrre2  8734  flqge  9124  monoord  9235