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  4248  swopo  4300  reusv3  4454  ralxfrd  4456  rexxfrd  4457  nlimsucg  4559  poirr2  5013  elpreima  5627  fmptco  5674  tposfo2  6258  nnm00  6521  th3qlem1  6627  fiintim  6918  supmoti  6982  infglbti  7014  infnlbti  7015  updjud  7071  recexprlemss1l  7609  recexprlemss1u  7610  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgprlemladdrl  7652  uzind  9337  ledivge1le  9697  xltnegi  9806  ixxssixx  9873  expnegzap  10524  shftlem  10793  cau3lem  11091  caubnd2  11094  climuni  11269  2clim  11277  summodclem2  11358  summodc  11359  zsumdc  11360  fsumf1o  11366  fisumss  11368  fsumcl2lem  11374  fsumadd  11382  fsummulc2  11424  prodmodclem2  11553  prodmodc  11554  zproddc  11555  fprodf1o  11564  fprodssdc  11566  fprodmul  11567  dfgcd2  11982  cncongrprm  12124  prmpwdvds  12320  infpnlem1  12324  1arith  12332  isgrpid2  12784  eltg3  13137  tgidm  13154  tgrest  13249  tgcn  13288  lmtopcnp  13330  txbasval  13347  txcnp  13351  bldisj  13481  xblm  13497  blssps  13507  blss  13508  blssexps  13509  blssex  13510  metcnp3  13591  2sqlem6  14036  2sqlem7  14037  bj-findis  14300