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  4272  swopo  4324  reusv3  4478  ralxfrd  4480  rexxfrd  4481  nlimsucg  4583  poirr2  5039  elpreima  5656  fmptco  5703  tposfo2  6292  nnm00  6555  th3qlem1  6663  fiintim  6957  supmoti  7022  infglbti  7054  infnlbti  7055  updjud  7111  recexprlemss1l  7664  recexprlemss1u  7665  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  caucvgprlemladdrl  7707  uzind  9394  ledivge1le  9756  xltnegi  9865  ixxssixx  9932  expnegzap  10585  shftlem  10857  cau3lem  11155  caubnd2  11158  climuni  11333  2clim  11341  summodclem2  11422  summodc  11423  zsumdc  11424  fsumf1o  11430  fisumss  11432  fsumcl2lem  11438  fsumadd  11446  fsummulc2  11488  prodmodclem2  11617  prodmodc  11618  zproddc  11619  fprodf1o  11628  fprodssdc  11630  fprodmul  11631  dfgcd2  12047  cncongrprm  12189  prmpwdvds  12387  infpnlem1  12391  1arith  12399  isgrpid2  12984  dvdsrd  13444  dvdsrtr  13451  dvdsrmul1  13452  unitgrp  13466  eltg3  14017  tgidm  14034  tgrest  14129  tgcn  14168  lmtopcnp  14210  txbasval  14227  txcnp  14231  bldisj  14361  xblm  14377  blssps  14387  blss  14388  blssexps  14389  blssex  14390  metcnp3  14471  2sqlem6  14928  2sqlem7  14929  bj-findis  15192