Theorem simp2bi 1146

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 1143	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:  0ellim  6396  smodm  8320  erdm  8681  ixpfn  8876  winafp  10650  inar1  10728  inatsk  10731  tskuni  10736  grur1  10773  supmullem1  12153  supmullem2  12154  supmul  12155  eluzelz  12803  elfz3nn0  13582  elfzo0l  13717  ico01fl0  13781  addmodlteq  13911  cshco  14802  swrds2  14906  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  bitsss  16396  smueqlem  16460  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  gzabssqcl  16912  4sqlem4a  16922  cshwshashlem2  17067  structn0fun  17121  xpsff1o  17530  mre1cl  17555  drsbn0  18265  subgss  19059  symgfixelsi  19365  psgnunilem5  19424  pgpgrp  19524  slwsubg  19540  efgs1b  19666  efgsp1  19667  efgsres  19668  efgredeu  19682  efgred2  19683  efgcpbllemb  19685  rngmgp  20065  srgmgp  20100  ringmgp  20148  irrednu  20334  sdrgsubrg  20700  fldsdrgfld  20707  sdrgint  20713  primefld  20714  primefld0cl  20715  primefld1cl  20716  lmodring  20774  lmodprop2d  20830  lssn0  20846  phlsrng  21540  ocvss  21579  obsss  21633  locfinbas  23409  fclsfil  23897  tmdtps  23963  tgptmd  23966  trgring  24058  tdrgdrng  24061  ngpms  24488  icopnfcnv  24840  xrhmeo  24844  oprpiece1res2  24850  phtpcer  24894  pcoval2  24916  pcoass  24924  clmsca  24965  cphsqrtcl  25084  bncms  25244  itg2ge0  25636  uc1pn0  26051  mon1pn0  26052  sinq12ge0  26417  cosq14gt0  26419  cosq14ge0  26420  cos02pilt1  26435  cosq34lt1  26436  sinord  26443  recosf1o  26444  resinf1o  26445  logrnaddcl  26483  logbcl  26677  relogbreexp  26685  atanf  26790  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  dvatan  26845  areambl  26868  rlimcnp  26875  emgt0  26917  harmoniclbnd  26919  harmonicbnd4  26921  lgamgulmlem2  26940  gausslemma2dlem1a  27276  2sqlem2  27329  2sqlem3  27331  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  logdivbnd  27467  pntpbnd2  27498  pnt  27525  brbtwn2  28832  ax5seglem3  28858  ax5seglem6  28861  axpaschlem  28867  axcontlem2  28892  axcontlem4  28894  crctcshwlkn0lem4  29743  wwlkbp  29771  clwwisshclwwslem  29943  hst1a  32147  stge0  32153  sthil  32163  neldifpr1  32462  f1mptrn  32559  cshwrnid  32883  fsumrp0cl  32962  omndtos  33019  fzo0pmtrlast  33049  wrdpmtrlast  33050  psgnfzto1stlem  33057  slmdsrg  33160  primefldchr  33251  fldgensdrg  33264  primefldgen1  33271  orngogrp  33279  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  elunitge0  33889  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iifiso  33925  rrextnlm  33993  rrextchr  33994  0elros  34160  0elsros  34167  voliune  34219  volfiniune  34220  bnj563  34733  bnj1212  34789  bnj1219  34790  bnj1366  34819  bnj1379  34820  bnj545  34885  bnj594  34902  bnj1118  34974  bnj1177  34996  bnj1190  34998  bnj1398  35024  bnj1417  35031  bnj1450  35040  bnj1312  35048  bnj1523  35061  pthhashvtx  35115  msrval  35525  mclsppslem  35570  dfon2lem1  35771  dfrdg2  35783  cntotbnd  37790  heiborlem5  37809  heiborlem6  37810  eqvrelsymrel  38590  atl0dm  39295  dalem-ccly  39679  stoweidlem60  46058  fourierdlem40  46145  fourierdlem78  46182  upgrimpthslem1  47907  usgrgrtrirex  47949  ackval40  48682