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  4320  swopo  4374  reusv3  4528  ralxfrd  4530  rexxfrd  4531  nlimsucg  4635  poirr2  5097  elpreima  5727  fmptco  5774  tposfo2  6383  nnm00  6646  th3qlem1  6754  fiintim  7061  supmoti  7128  infglbti  7160  infnlbti  7161  updjud  7217  recexprlemss1l  7790  recexprlemss1u  7791  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  caucvgprlemladdrl  7833  uzind  9526  ledivge1le  9890  xltnegi  9999  ixxssixx  10066  seqf1oglem1  10708  expnegzap  10762  shftlem  11293  cau3lem  11591  caubnd2  11594  climuni  11770  2clim  11778  summodclem2  11859  summodc  11860  zsumdc  11861  fsumf1o  11867  fisumss  11869  fsumcl2lem  11875  fsumadd  11883  fsummulc2  11925  prodmodclem2  12054  prodmodc  12055  zproddc  12056  fprodf1o  12065  fprodssdc  12067  fprodmul  12068  dfgcd2  12501  cncongrprm  12645  prmpwdvds  12844  infpnlem1  12848  1arith  12856  isgrpid2  13539  dvdsrd  14023  dvdsrtr  14030  dvdsrmul1  14031  unitgrp  14045  domnmuln0  14202  eltg3  14696  tgidm  14713  tgrest  14808  tgcn  14847  lmtopcnp  14889  txbasval  14906  txcnp  14910  bldisj  15040  xblm  15056  blssps  15066  blss  15067  blssexps  15068  blssex  15069  metcnp3  15150  mpomulcn  15205  2lgslem3  15745  2sqlem6  15764  2sqlem7  15765  bj-findis  16252