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  4559  rexxfrd  4560  elunirn  5907  onunsnss  7109  xpfi  7124  snon0  7134  genprndl  7741  genprndu  7742  addlsub  8549  letrp1  9028  peano2uz2  9587  uzind  9591  xrre  10055  xrre2  10056  flqge  10543  monoord  10748  facwordi  11003  facavg  11009  dvdsmultr1  12410  ltoddhalfle  12472  dvdsgcdb  12602  dfgcd2  12603  coprmgcdb  12678  coprmdvds2  12683  exprmfct  12728  prmdvdsfz  12729  prmfac1  12742  rpexp  12743  eulerthlemh  12821  pcpremul  12884  pcdvdsb  12911  pcprmpw2  12924  pockthlem  12947  4sqlem11  12992  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  lgsquad2lem2  15830