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  4303  swopo  4357  reusv3  4511  ralxfrd  4513  rexxfrd  4514  nlimsucg  4618  poirr2  5080  elpreima  5706  fmptco  5753  tposfo2  6360  nnm00  6623  th3qlem1  6731  fiintim  7035  supmoti  7102  infglbti  7134  infnlbti  7135  updjud  7191  recexprlemss1l  7755  recexprlemss1u  7756  cauappcvgprlemladdru  7776  cauappcvgprlemladdrl  7777  caucvgprlemladdrl  7798  uzind  9491  ledivge1le  9855  xltnegi  9964  ixxssixx  10031  seqf1oglem1  10671  expnegzap  10725  shftlem  11171  cau3lem  11469  caubnd2  11472  climuni  11648  2clim  11656  summodclem2  11737  summodc  11738  zsumdc  11739  fsumf1o  11745  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  fsummulc2  11803  prodmodclem2  11932  prodmodc  11933  zproddc  11934  fprodf1o  11943  fprodssdc  11945  fprodmul  11946  dfgcd2  12379  cncongrprm  12523  prmpwdvds  12722  infpnlem1  12726  1arith  12734  isgrpid2  13416  dvdsrd  13900  dvdsrtr  13907  dvdsrmul1  13908  unitgrp  13922  domnmuln0  14079  eltg3  14573  tgidm  14590  tgrest  14685  tgcn  14724  lmtopcnp  14766  txbasval  14783  txcnp  14787  bldisj  14917  xblm  14933  blssps  14943  blss  14944  blssexps  14945  blssex  14946  metcnp3  15027  mpomulcn  15082  2lgslem3  15622  2sqlem6  15641  2sqlem7  15642  bj-findis  15989