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  4341  swopo  4397  reusv3  4551  ralxfrd  4553  rexxfrd  4554  nlimsucg  4658  poirr2  5121  elpreima  5756  fmptco  5803  tposfo2  6419  nnm00  6684  th3qlem1  6792  fiintim  7101  supmoti  7168  infglbti  7200  infnlbti  7201  updjud  7257  recexprlemss1l  7830  recexprlemss1u  7831  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  uzind  9566  ledivge1le  9930  xltnegi  10039  ixxssixx  10106  seqf1oglem1  10749  expnegzap  10803  shftlem  11335  cau3lem  11633  caubnd2  11636  climuni  11812  2clim  11820  summodclem2  11901  summodc  11902  zsumdc  11903  fsumf1o  11909  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  prodmodclem2  12096  prodmodc  12097  zproddc  12098  fprodf1o  12107  fprodssdc  12109  fprodmul  12110  dfgcd2  12543  cncongrprm  12687  prmpwdvds  12886  infpnlem1  12890  1arith  12898  isgrpid2  13581  dvdsrd  14066  dvdsrtr  14073  dvdsrmul1  14074  unitgrp  14088  domnmuln0  14245  eltg3  14739  tgidm  14756  tgrest  14851  tgcn  14890  lmtopcnp  14932  txbasval  14949  txcnp  14953  bldisj  15083  xblm  15099  blssps  15109  blss  15110  blssexps  15111  blssex  15112  metcnp3  15193  mpomulcn  15248  2lgslem3  15788  2sqlem6  15807  2sqlem7  15808  uspgr2wlkeq  16086  wlklenvclwlk  16094  bj-findis  16366