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  4393  swopo  4449  reusv3  4604  ralxfrd  4606  rexxfrd  4607  nlimsucg  4711  poirr2  5178  elpreima  5822  fmptco  5868  suppssdc  6494  tposfo2  6532  nnm00  6797  th3qlem1  6905  fiintim  7232  supmoti  7327  infglbti  7359  infnlbti  7360  updjud  7416  recexprlemss1l  7996  recexprlemss1u  7997  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  uzind  9740  ledivge1le  10110  xltnegi  10220  ixxssixx  10287  seqf1oglem1  10939  expnegzap  10993  ccatrcl1  11365  shftlem  11564  cau3lem  11863  caubnd2  11866  climuni  12042  2clim  12050  summodclem2  12132  summodc  12133  zsumdc  12134  fsumf1o  12140  fisumss  12142  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodf1o  12338  fprodssdc  12340  fprodmul  12341  dfgcd2  12774  cncongrprm  12918  prmpwdvds  13117  infpnlem1  13121  1arith  13129  isgrpid2  13828  dvdsrd  14384  dvdsrtr  14391  dvdsrmul1  14392  unitgrp  14406  domnmuln0  14565  eltg3  15141  tgidm  15158  tgrest  15253  tgcn  15292  lmtopcnp  15334  txbasval  15351  txcnp  15355  bldisj  15485  xblm  15501  blssps  15511  blss  15512  blssexps  15513  blssex  15514  metcnp3  15595  mpomulcn  15650  2lgslem3  16203  2sqlem6  16222  2sqlem7  16223  uspgr2wlkeq  16589  wlklenvclwlk  16597  clwwlkccatlem  16624  clwwlknonel  16656  bj-findis  16988