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  4373  swopo  4429  reusv3  4583  ralxfrd  4585  rexxfrd  4586  nlimsucg  4690  poirr2  5157  elpreima  5799  fmptco  5845  suppssdc  6462  tposfo2  6500  nnm00  6765  th3qlem1  6873  fiintim  7193  supmoti  7286  infglbti  7318  infnlbti  7319  updjud  7375  recexprlemss1l  7955  recexprlemss1u  7956  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  caucvgprlemladdrl  7998  uzind  9695  ledivge1le  10065  xltnegi  10174  ixxssixx  10241  seqf1oglem1  10888  expnegzap  10942  ccatrcl1  11310  shftlem  11509  cau3lem  11807  caubnd2  11810  climuni  11986  2clim  11994  summodclem2  12076  summodc  12077  zsumdc  12078  fsumf1o  12084  fisumss  12086  fsumcl2lem  12092  fsumadd  12100  fsummulc2  12142  prodmodclem2  12271  prodmodc  12272  zproddc  12273  fprodf1o  12282  fprodssdc  12284  fprodmul  12285  dfgcd2  12718  cncongrprm  12862  prmpwdvds  13061  infpnlem1  13065  1arith  13073  isgrpid2  13774  dvdsrd  14261  dvdsrtr  14268  dvdsrmul1  14269  unitgrp  14283  domnmuln0  14442  eltg3  14971  tgidm  14988  tgrest  15083  tgcn  15122  lmtopcnp  15164  txbasval  15181  txcnp  15185  bldisj  15315  xblm  15331  blssps  15341  blss  15342  blssexps  15343  blssex  15344  metcnp3  15425  mpomulcn  15480  2lgslem3  16023  2sqlem6  16042  2sqlem7  16043  uspgr2wlkeq  16409  wlklenvclwlk  16417  clwwlkccatlem  16444  clwwlknonel  16476  bj-findis  16798