Theorem simp2bi 1145

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2bi	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1142	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  smodm  8389  erdm  8753  ixpfn  8941  winafp  10734  inar1  10812  inatsk  10815  tskuni  10820  grur1  10857  supmullem1  12235  supmullem2  12236  supmul  12237  eluzelz  12885  elfz3nn0  13657  elfzo0l  13791  ico01fl0  13855  addmodlteq  13983  cshco  14871  swrds2  14975  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  bitsss  16459  smueqlem  16523  gznegcl  16968  gzcjcl  16969  gzaddcl  16970  gzmulcl  16971  gzabssqcl  16974  4sqlem4a  16984  cshwshashlem2  17130  structn0fun  17184  xpsff1o  17613  mre1cl  17638  drsbn0  18361  subgss  19157  symgfixelsi  19467  psgnunilem5  19526  pgpgrp  19626  slwsubg  19642  efgs1b  19768  efgsp1  19769  efgsres  19770  efgredeu  19784  efgred2  19785  efgcpbllemb  19787  rngmgp  20173  srgmgp  20208  ringmgp  20256  irrednu  20441  sdrgsubrg  20808  fldsdrgfld  20815  sdrgint  20821  primefld  20822  primefld0cl  20823  primefld1cl  20824  lmodring  20882  lmodprop2d  20938  lssn0  20955  phlsrng  21666  ocvss  21705  obsss  21761  locfinbas  23545  fclsfil  24033  tmdtps  24099  tgptmd  24102  trgring  24194  tdrgdrng  24197  ngpms  24628  icopnfcnv  24986  xrhmeo  24990  oprpiece1res2  24996  phtpcer  25040  pcoval2  25062  pcoass  25070  clmsca  25111  cphsqrtcl  25231  bncms  25391  itg2ge0  25784  uc1pn0  26199  mon1pn0  26200  sinq12ge0  26564  cosq14gt0  26566  cosq14ge0  26567  cos02pilt1  26582  cosq34lt1  26583  sinord  26590  recosf1o  26591  resinf1o  26592  logrnaddcl  26630  logbcl  26824  relogbreexp  26832  atanf  26937  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  dvatan  26992  areambl  27015  rlimcnp  27022  emgt0  27064  harmoniclbnd  27066  harmonicbnd4  27068  lgamgulmlem2  27087  gausslemma2dlem1a  27423  2sqlem2  27476  2sqlem3  27478  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  logdivbnd  27614  pntpbnd2  27645  pnt  27672  brbtwn2  28934  ax5seglem3  28960  ax5seglem6  28963  axpaschlem  28969  axcontlem2  28994  axcontlem4  28996  crctcshwlkn0lem4  29842  wwlkbp  29870  clwwisshclwwslem  30042  hst1a  32246  stge0  32252  sthil  32262  neldifpr1  32558  f1mptrn  32651  cshwrnid  32930  fsumrp0cl  33008  omndtos  33064  fzo0pmtrlast  33094  wrdpmtrlast  33095  psgnfzto1stlem  33102  slmdsrg  33195  primefldchr  33282  fldgensdrg  33295  primefldgen1  33302  orngogrp  33310  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  elunitge0  33859  xrge0iifcnv  33893  xrge0iifcv  33894  xrge0iifiso  33895  rrextnlm  33965  rrextchr  33966  0elros  34150  0elsros  34157  voliune  34209  volfiniune  34210  bnj563  34735  bnj1212  34791  bnj1219  34792  bnj1366  34821  bnj1379  34822  bnj545  34887  bnj594  34904  bnj1118  34976  bnj1177  34998  bnj1190  35000  bnj1398  35026  bnj1417  35033  bnj1450  35042  bnj1312  35050  bnj1523  35063  pthhashvtx  35111  msrval  35522  mclsppslem  35567  dfon2lem1  35764  dfrdg2  35776  cntotbnd  37782  heiborlem5  37801  heiborlem6  37802  eqvrelsymrel  38580  atl0dm  39283  dalem-ccly  39667  stoweidlem60  46015  fourierdlem40  46102  fourierdlem78  46139  uspgrimprop  47810  usgrgrtrirex  47852  ackval40  48542