Theorem simp2bi 1164

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 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1161	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  0ellim  6427  smodm  8363  erdm  8732  ixpfn  8935  winafp  10786  inar1  10864  inatsk  10867  tskuni  10872  grur1  10909  supmullem1  12291  supmullem2  12292  supmul  12293  eluzelz  12979  elfz3nn0  13759  elfzo0l  13895  ico01fl0  13963  addmodlteq  14093  cshco  14992  swrds2  15097  ef01bndlem  16358  sin01bnd  16359  cos01bnd  16360  sin01gt0  16364  bitsss  16602  smueqlem  16666  gznegcl  17119  gzcjcl  17120  gzaddcl  17121  gzmulcl  17122  gzabssqcl  17125  4sqlem4a  17135  cshwshashlem2  17280  structn0fun  17335  xpsff1o  17745  mre1cl  17770  drsbn0  18484  subgss  19343  symgfixelsi  19655  psgnunilem5  19714  pgpgrp  19814  slwsubg  19830  efgs1b  19956  efgsp1  19957  efgsres  19958  efgredeu  19972  efgred2  19973  efgcpbllemb  19975  omndtos  20347  rngmgp  20384  srgmgp  20423  ringmgp  20471  irrednu  20661  sdrgsubrg  21054  fldsdrgfld  21061  sdrgint  21067  primefld  21068  primefld0cl  21069  primefld1cl  21070  orngogrp  21126  lmodring  21149  lmodprop2d  21205  lssn0  21221  phlsrng  21943  ocvss  21982  obsss  22036  locfinbas  23847  fclsfil  24335  tmdtps  24401  tgptmd  24404  trgring  24496  tdrgdrng  24499  ngpms  24925  icopnfcnv  25269  xrhmeo  25273  oprpiece1res2  25279  phtpcer  25322  pcoval2  25343  pcoass  25351  clmsca  25392  cphsqrtcl  25511  bncms  25671  itg2ge0  26062  uc1pn0  26470  mon1pn0  26471  sinq12ge0  26843  cosq14gt0  26845  cosq14ge0  26846  cos02pilt1  26860  cosq34lt1  26861  sinord  26868  recosf1o  26869  resinf1o  26870  logrnaddcl  26908  logbcl  27101  relogbreexp  27109  atanf  27214  atanneg  27241  atancj  27244  efiatan  27246  atanlogaddlem  27247  atanlogadd  27248  atanlogsub  27250  efiatan2  27251  2efiatan  27252  tanatan  27253  dvatan  27269  areambl  27292  rlimcnp  27299  emgt0  27340  harmoniclbnd  27342  harmonicbnd4  27344  lgamgulmlem2  27363  gausslemma2dlem1a  27698  2sqlem2  27751  2sqlem3  27753  dchrvmasumlem2  27831  dchrvmasumiflem1  27834  logdivbnd  27889  pntpbnd2  27920  pnt  27947  brbtwn2  29489  ax5seglem3  29515  ax5seglem6  29518  axpaschlem  29524  axcontlem2  29549  axcontlem4  29551  pthhashvtx  30321  crctcshwlkn0lem4  30408  wwlkbp  30436  clwwisshclwwslem  30611  hst1a  32826  stge0  32832  sthil  32842  neldifpr1  33177  f1mptrn  33277  cshwrnid  33569  fsumrp0cl  33629  fzo0pmtrlast  33700  wrdpmtrlast  33701  psgnfzto1stlem  33708  slmdsrg  33815  primefldchr  33910  fldgensdrg  33923  primefldgen1  33930  1arithidomlem1  34114  1arithidomlem2  34115  1arithidom  34116  elunitge0  34578  xrge0iifcnv  34612  xrge0iifcv  34613  xrge0iifiso  34614  rrextnlm  34682  rrextchr  34683  0elros  34850  0elsros  34857  voliune  34909  volfiniune  34910  bnj563  35421  bnj1212  35476  bnj1219  35477  bnj1366  35506  bnj1379  35507  bnj545  35572  bnj594  35589  bnj1118  35661  bnj1177  35683  bnj1190  35685  bnj1398  35711  bnj1417  35718  bnj1450  35727  bnj1312  35735  bnj1523  35748  msrval  36390  mclsppslem  36435  dfrdg2  36650  cntotbnd  38824  heiborlem5  38843  heiborlem6  38844  eqvrelsymrel  39709  atl0dm  40453  dalem-ccly  40836  stoweidlem60  47164  fourierdlem40  47251  fourierdlem78  47288  upgrimpthslem1  49099  usgrgrtrirex  49142  ackval40  49899