Theorem expimpd 358

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 114	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 252	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  euotd  4136  swopo  4188  reusv3  4341  ralxfrd  4343  rexxfrd  4344  nlimsucg  4441  poirr2  4889  elpreima  5493  fmptco  5540  tposfo2  6118  nnm00  6379  th3qlem1  6485  fiintim  6770  supmoti  6832  infglbti  6864  infnlbti  6865  updjud  6919  recexprlemss1l  7391  recexprlemss1u  7392  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemladdrl  7434  uzind  9066  ledivge1le  9412  xltnegi  9511  ixxssixx  9578  expnegzap  10220  shftlem  10481  cau3lem  10778  caubnd2  10781  climuni  10954  2clim  10962  summodclem2  11043  summodc  11044  zsumdc  11045  fsumf1o  11051  fisumss  11053  fsumcl2lem  11059  fsumadd  11067  fsummulc2  11109  dfgcd2  11548  cncongrprm  11681  eltg3  12069  tgidm  12086  tgrest  12181  tgcn  12219  lmtopcnp  12261  txbasval  12278  txcnp  12282  bldisj  12390  xblm  12406  blssps  12416  blss  12417  blssexps  12418  blssex  12419  metcnp3  12500  bj-findis  12869