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  4345  swopo  4401  reusv3  4555  ralxfrd  4557  rexxfrd  4558  nlimsucg  4662  poirr2  5127  elpreima  5762  fmptco  5809  tposfo2  6428  nnm00  6693  th3qlem1  6801  fiintim  7118  supmoti  7186  infglbti  7218  infnlbti  7219  updjud  7275  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  uzind  9584  ledivge1le  9954  xltnegi  10063  ixxssixx  10130  seqf1oglem1  10774  expnegzap  10828  ccatrcl1  11184  shftlem  11370  cau3lem  11668  caubnd2  11671  climuni  11847  2clim  11855  summodclem2  11936  summodc  11937  zsumdc  11938  fsumf1o  11944  fisumss  11946  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodf1o  12142  fprodssdc  12144  fprodmul  12145  dfgcd2  12578  cncongrprm  12722  prmpwdvds  12921  infpnlem1  12925  1arith  12933  isgrpid2  13616  dvdsrd  14101  dvdsrtr  14108  dvdsrmul1  14109  unitgrp  14123  domnmuln0  14280  eltg3  14774  tgidm  14791  tgrest  14886  tgcn  14925  lmtopcnp  14967  txbasval  14984  txcnp  14988  bldisj  15118  xblm  15134  blssps  15144  blss  15145  blssexps  15146  blssex  15147  metcnp3  15228  mpomulcn  15283  2lgslem3  15823  2sqlem6  15842  2sqlem7  15843  uspgr2wlkeq  16176  wlklenvclwlk  16184  clwwlkccatlem  16209  clwwlknonel  16241  bj-findis  16524