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  4493  rexxfrd  4494  elunirn  5809  onunsnss  6973  xpfi  6986  snon0  6994  genprndl  7581  genprndu  7582  addlsub  8389  letrp1  8867  peano2uz2  9424  uzind  9428  xrre  9886  xrre2  9887  flqge  10351  monoord  10556  facwordi  10811  facavg  10817  dvdsmultr1  11974  ltoddhalfle  12034  dvdsgcdb  12150  dfgcd2  12151  coprmgcdb  12226  coprmdvds2  12231  exprmfct  12276  prmdvdsfz  12277  prmfac1  12290  rpexp  12291  eulerthlemh  12369  pcpremul  12431  pcdvdsb  12458  pcprmpw2  12471  pockthlem  12494  4sqlem11  12539  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191