Theorem mpan2d 432

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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpand  433  mpan2i  435  ralxfrd  4608  rexxfrd  4609  elunirn  5972  onunsnss  7224  xpfi  7239  snon0  7249  genprndl  7888  genprndu  7889  addlsub  8697  letrp1  9180  peano2uz2  9757  uzind  9761  xrre  10232  xrre2  10233  flqge  10729  flapge  10730  monoord  10935  facwordi  11192  facavg  11198  dvdsmultr1  12614  ltoddhalfle  12676  dvdsgcdb  12806  dfgcd2  12807  coprmgcdb  12882  coprmdvds2  12887  exprmfct  12933  prmdvdsfz  12934  prmfac1  12947  rpexp  12948  eulerthlemh  13029  pcpremul  13092  pcdvdsb  13119  pcprmpw2  13132  pockthlem  13155  4sqlem11  13200  bposlem3  16211  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  lgsquad2lem2  16299