Theorem mpan2d 428

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mpan2d.1	⊢ (𝜑 → 𝜒)
mpan2d.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpan2d	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpan2d

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mpan2d.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 258	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 42	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  7087  xpfi  7102  snon0  7110  genprndl  7716  genprndu  7717  addlsub  8524  letrp1  9003  peano2uz2  9562  uzind  9566  xrre  10024  xrre2  10025  flqge  10510  monoord  10715  facwordi  10970  facavg  10976  dvdsmultr1  12350  ltoddhalfle  12412  dvdsgcdb  12542  dfgcd2  12543  coprmgcdb  12618  coprmdvds2  12623  exprmfct  12668  prmdvdsfz  12669  prmfac1  12682  rpexp  12683  eulerthlemh  12761  pcpremul  12824  pcdvdsb  12851  pcprmpw2  12864  pockthlem  12887  4sqlem11  12932  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  lgseisenlem1  15757  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem1  15768  lgsquad2lem2  15769