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  4349  swopo  4405  reusv3  4559  ralxfrd  4561  rexxfrd  4562  nlimsucg  4666  poirr2  5131  elpreima  5769  fmptco  5816  tposfo2  6438  nnm00  6703  th3qlem1  6811  fiintim  7128  supmoti  7197  infglbti  7229  infnlbti  7230  updjud  7286  recexprlemss1l  7860  recexprlemss1u  7861  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  caucvgprlemladdrl  7903  uzind  9596  ledivge1le  9966  xltnegi  10075  ixxssixx  10142  seqf1oglem1  10787  expnegzap  10841  ccatrcl1  11200  shftlem  11399  cau3lem  11697  caubnd2  11700  climuni  11876  2clim  11884  summodclem2  11966  summodc  11967  zsumdc  11968  fsumf1o  11974  fisumss  11976  fsumcl2lem  11982  fsumadd  11990  fsummulc2  12032  prodmodclem2  12161  prodmodc  12162  zproddc  12163  fprodf1o  12172  fprodssdc  12174  fprodmul  12175  dfgcd2  12608  cncongrprm  12752  prmpwdvds  12951  infpnlem1  12955  1arith  12963  isgrpid2  13646  dvdsrd  14132  dvdsrtr  14139  dvdsrmul1  14140  unitgrp  14154  domnmuln0  14311  eltg3  14810  tgidm  14827  tgrest  14922  tgcn  14961  lmtopcnp  15003  txbasval  15020  txcnp  15024  bldisj  15154  xblm  15170  blssps  15180  blss  15181  blssexps  15182  blssex  15183  metcnp3  15264  mpomulcn  15319  2lgslem3  15859  2sqlem6  15878  2sqlem7  15879  uspgr2wlkeq  16245  wlklenvclwlk  16253  clwwlkccatlem  16280  clwwlknonel  16312  bj-findis  16634