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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  euotd  4397  swopo  4453  reusv3  4608  ralxfrd  4610  rexxfrd  4611  nlimsucg  4715  poirr2  5183  elpreima  5831  fmptco  5877  suppssdc  6504  tposfo2  6542  nnm00  6807  th3qlem1  6915  fiintim  7243  supmoti  7340  infglbti  7372  infnlbti  7373  updjud  7429  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  uzind  9769  ledivge1le  10145  xltnegi  10255  ixxssixx  10322  seqf1oglem1  10978  expnegzap  11032  ccatrcl1  11405  shftlem  11604  cau3lem  11904  caubnd2  11907  climuni  12085  2clim  12093  summodclem2  12175  summodc  12176  zsumdc  12177  fsumf1o  12183  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  prodmodclem2  12370  prodmodc  12371  zproddc  12372  fprodf1o  12381  fprodssdc  12383  fprodmul  12384  dfgcd2  12817  cncongrprm  12962  prmpwdvds  13164  infpnlem1  13168  1arith  13176  prmlem0  13250  isgrpid2  13905  dvdsrd  14511  dvdsrtr  14518  dvdsrmul1  14519  unitgrp  14533  domnmuln0  14692  eltg3  15295  tgidm  15312  tgrest  15407  tgcn  15446  lmtopcnp  15488  txbasval  15505  txcnp  15509  bldisj  15639  xblm  15655  blssps  15665  blss  15666  blssexps  15667  blssex  15668  metcnp3  15749  mpomulcn  15804  rpcxpmul2z  16160  2lgslem3  16437  2sqlem6  16456  2sqlem7  16457  uspgr2wlkeq  16823  wlklenvclwlk  16831  clwwlkccatlem  16858  clwwlknonel  16890  bj-findis  17222