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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  euotd  4397  swopo  4453  reusv3  4608  ralxfrd  4610  rexxfrd  4611  nlimsucg  4715  poirr2  5183  elpreima  5831  fmptco  5877  suppssdc  6504  tposfo2  6543  nnm00  6808  th3qlem1  6916  fiintim  7244  supmoti  7340  infglbti  7372  infnlbti  7373  updjud  7429  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  uzind  9768  ledivge1le  10144  xltnegi  10254  ixxssixx  10321  seqf1oglem1  10977  expnegzap  11031  ccatrcl1  11404  shftlem  11603  cau3lem  11903  caubnd2  11906  climuni  12084  2clim  12092  summodclem2  12174  summodc  12175  zsumdc  12176  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  dfgcd2  12816  cncongrprm  12961  prmpwdvds  13163  infpnlem1  13167  1arith  13175  prmlem0  13249  isgrpid2  13904  dvdsrd  14510  dvdsrtr  14517  dvdsrmul1  14518  unitgrp  14532  domnmuln0  14691  eltg3  15316  tgidm  15333  tgrest  15428  tgcn  15467  lmtopcnp  15509  txbasval  15526  txcnp  15530  bldisj  15660  xblm  15676  blssps  15686  blss  15687  blssexps  15688  blssex  15689  metcnp3  15770  mpomulcn  15825  rpcxpmul2z  16181  2lgslem3  16458  2sqlem6  16477  2sqlem7  16478  uspgr2wlkeq  16844  wlklenvclwlk  16852  clwwlkccatlem  16879  clwwlknonel  16911  bj-findis  17243