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  4370  swopo  4426  reusv3  4580  ralxfrd  4582  rexxfrd  4583  nlimsucg  4687  poirr2  5154  elpreima  5796  fmptco  5842  suppssdc  6459  tposfo2  6497  nnm00  6762  th3qlem1  6870  fiintim  7190  supmoti  7283  infglbti  7315  infnlbti  7316  updjud  7372  recexprlemss1l  7946  recexprlemss1u  7947  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  caucvgprlemladdrl  7989  uzind  9685  ledivge1le  10055  xltnegi  10164  ixxssixx  10231  seqf1oglem1  10877  expnegzap  10931  ccatrcl1  11295  shftlem  11494  cau3lem  11792  caubnd2  11795  climuni  11971  2clim  11979  summodclem2  12061  summodc  12062  zsumdc  12063  fsumf1o  12069  fisumss  12071  fsumcl2lem  12077  fsumadd  12085  fsummulc2  12127  prodmodclem2  12256  prodmodc  12257  zproddc  12258  fprodf1o  12267  fprodssdc  12269  fprodmul  12270  dfgcd2  12703  cncongrprm  12847  prmpwdvds  13046  infpnlem1  13050  1arith  13058  isgrpid2  13742  dvdsrd  14228  dvdsrtr  14235  dvdsrmul1  14236  unitgrp  14250  domnmuln0  14408  eltg3  14909  tgidm  14926  tgrest  15021  tgcn  15060  lmtopcnp  15102  txbasval  15119  txcnp  15123  bldisj  15253  xblm  15269  blssps  15279  blss  15280  blssexps  15281  blssex  15282  metcnp3  15363  mpomulcn  15418  2lgslem3  15961  2sqlem6  15980  2sqlem7  15981  uspgr2wlkeq  16347  wlklenvclwlk  16355  clwwlkccatlem  16382  clwwlknonel  16414  bj-findis  16736