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  4370  swopo  4426  reusv3  4580  ralxfrd  4582  rexxfrd  4583  nlimsucg  4687  poirr2  5154  elpreima  5796  fmptco  5842  suppssdc  6459  tposfo2  6497  nnm00  6762  th3qlem1  6870  fiintim  7190  supmoti  7283  infglbti  7315  infnlbti  7316  updjud  7372  recexprlemss1l  7949  recexprlemss1u  7950  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  caucvgprlemladdrl  7992  uzind  9688  ledivge1le  10058  xltnegi  10167  ixxssixx  10234  seqf1oglem1  10880  expnegzap  10934  ccatrcl1  11298  shftlem  11497  cau3lem  11795  caubnd2  11798  climuni  11974  2clim  11982  summodclem2  12064  summodc  12065  zsumdc  12066  fsumf1o  12072  fisumss  12074  fsumcl2lem  12080  fsumadd  12088  fsummulc2  12130  prodmodclem2  12259  prodmodc  12260  zproddc  12261  fprodf1o  12270  fprodssdc  12272  fprodmul  12273  dfgcd2  12706  cncongrprm  12850  prmpwdvds  13049  infpnlem1  13053  1arith  13061  isgrpid2  13745  dvdsrd  14231  dvdsrtr  14238  dvdsrmul1  14239  unitgrp  14253  domnmuln0  14411  eltg3  14914  tgidm  14931  tgrest  15026  tgcn  15065  lmtopcnp  15107  txbasval  15124  txcnp  15128  bldisj  15258  xblm  15274  blssps  15284  blss  15285  blssexps  15286  blssex  15287  metcnp3  15368  mpomulcn  15423  2lgslem3  15966  2sqlem6  15985  2sqlem7  15986  uspgr2wlkeq  16352  wlklenvclwlk  16360  clwwlkccatlem  16387  clwwlknonel  16419  bj-findis  16741