Theorem mpan2d 432

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 ⊢ (𝜑 → (𝜓 → 𝜃))

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  7889  genprndu  7890  addlsub  8698  letrp1  9181  peano2uz2  9758  uzind  9762  xrre  10233  xrre2  10234  flqge  10730  flapge  10731  monoord  10936  facwordi  11193  facavg  11199  dvdsmultr1  12616  ltoddhalfle  12678  dvdsgcdb  12808  dfgcd2  12809  coprmgcdb  12884  coprmdvds2  12889  exprmfct  12935  prmdvdsfz  12936  prmfac1  12949  rpexp  12950  eulerthlemh  13031  pcpremul  13094  pcdvdsb  13121  pcprmpw2  13134  pockthlem  13157  4sqlem11  13202  chtqub  16218  bposlem3  16235  lgsne0  16279  gausslemma2dlem1a  16299  gausslemma2dlem2  16303  lgseisenlem1  16311  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2lem1  16322  lgsquad2lem2  16323