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  4424  rexxfrd  4425  elunirn  5718  onunsnss  6863  xpfi  6876  snon0  6882  genprndl  7443  genprndu  7444  addlsub  8249  letrp1  8724  peano2uz2  9276  uzind  9280  xrre  9730  xrre2  9731  flqge  10190  monoord  10384  facwordi  10625  facavg  10631  dvdsmultr1  11737  ltoddhalfle  11796  dvdsgcdb  11912  dfgcd2  11913  coprmgcdb  11980  coprmdvds2  11985  exprmfct  12030  prmdvdsfz  12031  prmfac1  12042  rpexp  12043  eulerthlemh  12121  pcpremul  12183