Theorem expimpd 355

Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)

Hypothesis

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

Assertion

Ref	Expression
expimpd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 113	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 251	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  euotd  4038  swopo  4090  reusv3  4239  ralxfrd  4241  rexxfrd  4242  nlimsucg  4338  poirr2  4768  elpreima  5340  fmptco  5384  tposfo2  5938  nnm00  6191  th3qlem1  6297  supmoti  6502  infglbti  6534  infnlbti  6535  updjud  6577  recexprlemss1l  6964  recexprlemss1u  6965  cauappcvgprlemladdru  6985  cauappcvgprlemladdrl  6986  caucvgprlemladdrl  7007  uzind  8616  ledivge1le  8961  xltnegi  9055  ixxssixx  9078  expnegzap  9684  shftlem  9930  cau3lem  10226  caubnd2  10229  climuni  10358  2clim  10366  dfgcd2  10635  cncongrprm  10768  bj-findis  11066