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  4395  swopo  4451  reusv3  4606  ralxfrd  4608  rexxfrd  4609  nlimsucg  4713  poirr2  5180  elpreima  5828  fmptco  5874  suppssdc  6500  tposfo2  6538  nnm00  6803  th3qlem1  6911  fiintim  7238  supmoti  7333  infglbti  7365  infnlbti  7366  updjud  7422  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  uzind  9759  ledivge1le  10129  xltnegi  10239  ixxssixx  10306  seqf1oglem1  10958  expnegzap  11012  ccatrcl1  11384  shftlem  11583  cau3lem  11882  caubnd2  11885  climuni  12061  2clim  12069  summodclem2  12151  summodc  12152  zsumdc  12153  fsumf1o  12159  fisumss  12161  fsumcl2lem  12167  fsumadd  12175  fsummulc2  12217  prodmodclem2  12346  prodmodc  12347  zproddc  12348  fprodf1o  12357  fprodssdc  12359  fprodmul  12360  dfgcd2  12793  cncongrprm  12937  prmpwdvds  13136  infpnlem1  13140  1arith  13148  isgrpid2  13847  dvdsrd  14403  dvdsrtr  14410  dvdsrmul1  14411  unitgrp  14425  domnmuln0  14584  eltg3  15160  tgidm  15177  tgrest  15272  tgcn  15311  lmtopcnp  15353  txbasval  15370  txcnp  15374  bldisj  15504  xblm  15520  blssps  15530  blss  15531  blssexps  15532  blssex  15533  metcnp3  15614  mpomulcn  15669  2lgslem3  16232  2sqlem6  16251  2sqlem7  16252  uspgr2wlkeq  16618  wlklenvclwlk  16626  clwwlkccatlem  16653  clwwlknonel  16685  bj-findis  17017