Theorem mpan2d 428

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpand  429  mpan2i  431  ralxfrd  4464  rexxfrd  4465  elunirn  5769  onunsnss  6918  xpfi  6931  snon0  6937  genprndl  7522  genprndu  7523  addlsub  8329  letrp1  8807  peano2uz2  9362  uzind  9366  xrre  9822  xrre2  9823  flqge  10284  monoord  10478  facwordi  10722  facavg  10728  dvdsmultr1  11840  ltoddhalfle  11900  dvdsgcdb  12016  dfgcd2  12017  coprmgcdb  12090  coprmdvds2  12095  exprmfct  12140  prmdvdsfz  12141  prmfac1  12154  rpexp  12155  eulerthlemh  12233  pcpremul  12295  pcdvdsb  12321  pcprmpw2  12334  pockthlem  12356  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490