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  4288  swopo  4342  reusv3  4496  ralxfrd  4498  rexxfrd  4499  nlimsucg  4603  poirr2  5063  elpreima  5684  fmptco  5731  tposfo2  6334  nnm00  6597  th3qlem1  6705  fiintim  7001  supmoti  7068  infglbti  7100  infnlbti  7101  updjud  7157  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  uzind  9456  ledivge1le  9820  xltnegi  9929  ixxssixx  9996  seqf1oglem1  10630  expnegzap  10684  shftlem  11000  cau3lem  11298  caubnd2  11301  climuni  11477  2clim  11485  summodclem2  11566  summodc  11567  zsumdc  11568  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  dfgcd2  12208  cncongrprm  12352  prmpwdvds  12551  infpnlem1  12555  1arith  12563  isgrpid2  13244  dvdsrd  13728  dvdsrtr  13735  dvdsrmul1  13736  unitgrp  13750  domnmuln0  13907  eltg3  14379  tgidm  14396  tgrest  14491  tgcn  14530  lmtopcnp  14572  txbasval  14589  txcnp  14593  bldisj  14723  xblm  14739  blssps  14749  blss  14750  blssexps  14751  blssex  14752  metcnp3  14833  mpomulcn  14888  2lgslem3  15428  2sqlem6  15447  2sqlem7  15448  bj-findis  15711