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  4342  swopo  4398  reusv3  4552  ralxfrd  4554  rexxfrd  4555  nlimsucg  4659  poirr2  5124  elpreima  5759  fmptco  5806  tposfo2  6424  nnm00  6689  th3qlem1  6797  fiintim  7109  supmoti  7176  infglbti  7208  infnlbti  7209  updjud  7265  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  uzind  9574  ledivge1le  9939  xltnegi  10048  ixxssixx  10115  seqf1oglem1  10758  expnegzap  10812  ccatrcl1  11167  shftlem  11348  cau3lem  11646  caubnd2  11649  climuni  11825  2clim  11833  summodclem2  11914  summodc  11915  zsumdc  11916  fsumf1o  11922  fisumss  11924  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodf1o  12120  fprodssdc  12122  fprodmul  12123  dfgcd2  12556  cncongrprm  12700  prmpwdvds  12899  infpnlem1  12903  1arith  12911  isgrpid2  13594  dvdsrd  14079  dvdsrtr  14086  dvdsrmul1  14087  unitgrp  14101  domnmuln0  14258  eltg3  14752  tgidm  14769  tgrest  14864  tgcn  14903  lmtopcnp  14945  txbasval  14962  txcnp  14966  bldisj  15096  xblm  15112  blssps  15122  blss  15123  blssexps  15124  blssex  15125  metcnp3  15206  mpomulcn  15261  2lgslem3  15801  2sqlem6  15820  2sqlem7  15821  uspgr2wlkeq  16137  wlklenvclwlk  16145  clwwlkccatlem  16169  bj-findis  16451