Theorem expimpd 361

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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  euotd  4209  swopo  4261  reusv3  4414  ralxfrd  4416  rexxfrd  4417  nlimsucg  4519  poirr2  4971  elpreima  5579  fmptco  5626  tposfo2  6204  nnm00  6465  th3qlem1  6571  fiintim  6862  supmoti  6925  infglbti  6957  infnlbti  6958  updjud  7012  recexprlemss1l  7534  recexprlemss1u  7535  cauappcvgprlemladdru  7555  cauappcvgprlemladdrl  7556  caucvgprlemladdrl  7577  uzind  9254  ledivge1le  9611  xltnegi  9717  ixxssixx  9784  expnegzap  10431  shftlem  10693  cau3lem  10991  caubnd2  10994  climuni  11167  2clim  11175  summodclem2  11256  summodc  11257  zsumdc  11258  fsumf1o  11264  fisumss  11266  fsumcl2lem  11272  fsumadd  11280  fsummulc2  11322  prodmodclem2  11451  prodmodc  11452  zproddc  11453  fprodf1o  11462  fprodssdc  11464  fprodmul  11465  dfgcd2  11869  cncongrprm  12002  eltg3  12396  tgidm  12413  tgrest  12508  tgcn  12547  lmtopcnp  12589  txbasval  12606  txcnp  12610  bldisj  12740  xblm  12756  blssps  12766  blss  12767  blssexps  12768  blssex  12769  metcnp3  12850  bj-findis  13492