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  4347  swopo  4403  reusv3  4557  ralxfrd  4559  rexxfrd  4560  nlimsucg  4664  poirr2  5129  elpreima  5766  fmptco  5813  tposfo2  6433  nnm00  6698  th3qlem1  6806  fiintim  7123  supmoti  7192  infglbti  7224  infnlbti  7225  updjud  7281  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  uzind  9591  ledivge1le  9961  xltnegi  10070  ixxssixx  10137  seqf1oglem1  10782  expnegzap  10836  ccatrcl1  11192  shftlem  11378  cau3lem  11676  caubnd2  11679  climuni  11855  2clim  11863  summodclem2  11945  summodc  11946  zsumdc  11947  fsumf1o  11953  fisumss  11955  fsumcl2lem  11961  fsumadd  11969  fsummulc2  12011  prodmodclem2  12140  prodmodc  12141  zproddc  12142  fprodf1o  12151  fprodssdc  12153  fprodmul  12154  dfgcd2  12587  cncongrprm  12731  prmpwdvds  12930  infpnlem1  12934  1arith  12942  isgrpid2  13625  dvdsrd  14111  dvdsrtr  14118  dvdsrmul1  14119  unitgrp  14133  domnmuln0  14290  eltg3  14784  tgidm  14801  tgrest  14896  tgcn  14935  lmtopcnp  14977  txbasval  14994  txcnp  14998  bldisj  15128  xblm  15144  blssps  15154  blss  15155  blssexps  15156  blssex  15157  metcnp3  15238  mpomulcn  15293  2lgslem3  15833  2sqlem6  15852  2sqlem7  15853  uspgr2wlkeq  16219  wlklenvclwlk  16227  clwwlkccatlem  16254  clwwlknonel  16286  bj-findis  16595