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  4582  rexxfrd  4583  elunirn  5938  onunsnss  7176  xpfi  7191  snon0  7201  genprndl  7835  genprndu  7836  addlsub  8642  letrp1  9121  peano2uz2  9684  uzind  9688  xrre  10152  xrre2  10153  flqge  10641  monoord  10846  facwordi  11101  facavg  11107  dvdsmultr1  12513  ltoddhalfle  12575  dvdsgcdb  12705  dfgcd2  12706  coprmgcdb  12781  coprmdvds2  12786  exprmfct  12831  prmdvdsfz  12832  prmfac1  12845  rpexp  12846  eulerthlemh  12924  pcpremul  12987  pcdvdsb  13014  pcprmpw2  13027  pockthlem  13050  4sqlem11  13095  lgsne0  15903  gausslemma2dlem1a  15923  gausslemma2dlem2  15927  lgseisenlem1  15935  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  lgsquadlem3  15944  lgsquad2lem1  15946  lgsquad2lem2  15947