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  4072  swopo  4124  reusv3  4273  ralxfrd  4275  rexxfrd  4276  nlimsucg  4372  poirr2  4811  elpreima  5402  fmptco  5448  tposfo2  6014  nnm00  6268  th3qlem1  6374  supmoti  6667  infglbti  6699  infnlbti  6700  updjud  6752  recexprlemss1l  7173  recexprlemss1u  7174  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  uzind  8827  ledivge1le  9172  xltnegi  9266  ixxssixx  9289  expnegzap  9954  shftlem  10215  cau3lem  10512  caubnd2  10515  climuni  10645  2clim  10653  isummolem2  10736  isummo  10737  zisum  10738  fsumf1o  10746  fisumss  10748  fsumcl2lem  10755  fsumadd  10763  fsummulc2  10805  dfgcd2  11085  cncongrprm  11218  bj-findis  11520