Theorem expimpd 363

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  euotd  4312  swopo  4366  reusv3  4520  ralxfrd  4522  rexxfrd  4523  nlimsucg  4627  poirr2  5089  elpreima  5717  fmptco  5764  tposfo2  6371  nnm00  6634  th3qlem1  6742  fiintim  7049  supmoti  7116  infglbti  7148  infnlbti  7149  updjud  7205  recexprlemss1l  7778  recexprlemss1u  7779  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  caucvgprlemladdrl  7821  uzind  9514  ledivge1le  9878  xltnegi  9987  ixxssixx  10054  seqf1oglem1  10696  expnegzap  10750  shftlem  11212  cau3lem  11510  caubnd2  11513  climuni  11689  2clim  11697  summodclem2  11778  summodc  11779  zsumdc  11780  fsumf1o  11786  fisumss  11788  fsumcl2lem  11794  fsumadd  11802  fsummulc2  11844  prodmodclem2  11973  prodmodc  11974  zproddc  11975  fprodf1o  11984  fprodssdc  11986  fprodmul  11987  dfgcd2  12420  cncongrprm  12564  prmpwdvds  12763  infpnlem1  12767  1arith  12775  isgrpid2  13457  dvdsrd  13941  dvdsrtr  13948  dvdsrmul1  13949  unitgrp  13963  domnmuln0  14120  eltg3  14614  tgidm  14631  tgrest  14726  tgcn  14765  lmtopcnp  14807  txbasval  14824  txcnp  14828  bldisj  14958  xblm  14974  blssps  14984  blss  14985  blssexps  14986  blssex  14987  metcnp3  15068  mpomulcn  15123  2lgslem3  15663  2sqlem6  15682  2sqlem7  15683  bj-findis  16084