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  4553  rexxfrd  4554  elunirn  5896  onunsnss  7090  xpfi  7105  snon0  7113  genprndl  7719  genprndu  7720  addlsub  8527  letrp1  9006  peano2uz2  9565  uzind  9569  xrre  10028  xrre2  10029  flqge  10514  monoord  10719  facwordi  10974  facavg  10980  dvdsmultr1  12357  ltoddhalfle  12419  dvdsgcdb  12549  dfgcd2  12550  coprmgcdb  12625  coprmdvds2  12630  exprmfct  12675  prmdvdsfz  12676  prmfac1  12689  rpexp  12690  eulerthlemh  12768  pcpremul  12831  pcdvdsb  12858  pcprmpw2  12871  pockthlem  12894  4sqlem11  12939  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  lgseisenlem1  15764  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad2lem2  15776