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  4527  rexxfrd  4528  elunirn  5858  onunsnss  7040  xpfi  7055  snon0  7063  genprndl  7669  genprndu  7670  addlsub  8477  letrp1  8956  peano2uz2  9515  uzind  9519  xrre  9977  xrre2  9978  flqge  10462  monoord  10667  facwordi  10922  facavg  10928  dvdsmultr1  12257  ltoddhalfle  12319  dvdsgcdb  12449  dfgcd2  12450  coprmgcdb  12525  coprmdvds2  12530  exprmfct  12575  prmdvdsfz  12576  prmfac1  12589  rpexp  12590  eulerthlemh  12668  pcpremul  12731  pcdvdsb  12758  pcprmpw2  12771  pockthlem  12794  4sqlem11  12839  lgsne0  15630  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  lgseisenlem1  15662  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad2lem2  15674