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  4376  swopo  4432  reusv3  4586  ralxfrd  4588  rexxfrd  4589  nlimsucg  4693  poirr2  5160  elpreima  5802  fmptco  5848  suppssdc  6473  tposfo2  6511  nnm00  6776  th3qlem1  6884  fiintim  7204  supmoti  7297  infglbti  7329  infnlbti  7330  updjud  7386  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  uzind  9710  ledivge1le  10080  xltnegi  10190  ixxssixx  10257  seqf1oglem1  10908  expnegzap  10962  ccatrcl1  11330  shftlem  11529  cau3lem  11827  caubnd2  11830  climuni  12006  2clim  12014  summodclem2  12096  summodc  12097  zsumdc  12098  fsumf1o  12104  fisumss  12106  fsumcl2lem  12112  fsumadd  12120  fsummulc2  12162  prodmodclem2  12291  prodmodc  12292  zproddc  12293  fprodf1o  12302  fprodssdc  12304  fprodmul  12305  dfgcd2  12738  cncongrprm  12882  prmpwdvds  13081  infpnlem1  13085  1arith  13093  isgrpid2  13798  dvdsrd  14342  dvdsrtr  14349  dvdsrmul1  14350  unitgrp  14364  domnmuln0  14523  eltg3  15051  tgidm  15068  tgrest  15163  tgcn  15202  lmtopcnp  15244  txbasval  15261  txcnp  15265  bldisj  15395  xblm  15411  blssps  15421  blss  15422  blssexps  15423  blssex  15424  metcnp3  15505  mpomulcn  15560  2lgslem3  16103  2sqlem6  16122  2sqlem7  16123  uspgr2wlkeq  16489  wlklenvclwlk  16497  clwwlkccatlem  16524  clwwlknonel  16556  bj-findis  16888