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  4474  rexxfrd  4475  elunirn  5780  onunsnss  6930  xpfi  6943  snon0  6949  genprndl  7534  genprndu  7535  addlsub  8341  letrp1  8819  peano2uz2  9374  uzind  9378  xrre  9834  xrre2  9835  flqge  10296  monoord  10490  facwordi  10734  facavg  10740  dvdsmultr1  11852  ltoddhalfle  11912  dvdsgcdb  12028  dfgcd2  12029  coprmgcdb  12102  coprmdvds2  12107  exprmfct  12152  prmdvdsfz  12153  prmfac1  12166  rpexp  12167  eulerthlemh  12245  pcpremul  12307  pcdvdsb  12333  pcprmpw2  12346  pockthlem  12368  lgsne0  14735  lgseisenlem1  14746  lgseisenlem2  14747