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  7334  infglbti  7366  infnlbti  7367  updjud  7423  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  uzind  9762  ledivge1le  10138  xltnegi  10248  ixxssixx  10315  seqf1oglem1  10970  expnegzap  11024  ccatrcl1  11397  shftlem  11596  cau3lem  11896  caubnd2  11899  climuni  12077  2clim  12085  summodclem2  12167  summodc  12168  zsumdc  12169  fsumf1o  12175  fisumss  12177  fsumcl2lem  12183  fsumadd  12191  fsummulc2  12233  prodmodclem2  12362  prodmodc  12363  zproddc  12364  fprodf1o  12373  fprodssdc  12375  fprodmul  12376  dfgcd2  12809  cncongrprm  12954  prmpwdvds  13156  infpnlem1  13160  1arith  13168  prmlem0  13242  isgrpid2  13896  dvdsrd  14452  dvdsrtr  14459  dvdsrmul1  14460  unitgrp  14474  domnmuln0  14633  eltg3  15210  tgidm  15227  tgrest  15322  tgcn  15361  lmtopcnp  15403  txbasval  15420  txcnp  15424  bldisj  15554  xblm  15570  blssps  15580  blss  15581  blssexps  15582  blssex  15583  metcnp3  15664  mpomulcn  15719  2lgslem3  16342  2sqlem6  16361  2sqlem7  16362  uspgr2wlkeq  16728  wlklenvclwlk  16736  clwwlkccatlem  16763  clwwlknonel  16795  bj-findis  17127