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 1087

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 1089

This theorem is referenced by:  smodm  8407  erdm  8773  ixpfn  8961  winafp  10766  inar1  10844  inatsk  10847  tskuni  10852  grur1  10889  supmullem1  12265  supmullem2  12266  supmul  12267  eluzelz  12913  elfz3nn0  13678  elfzo0l  13806  ico01fl0  13870  addmodlteq  13997  cshco  14885  swrds2  14989  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  bitsss  16472  smueqlem  16536  gznegcl  16982  gzcjcl  16983  gzaddcl  16984  gzmulcl  16985  gzabssqcl  16988  4sqlem4a  16998  cshwshashlem2  17144  structn0fun  17198  xpsff1o  17627  mre1cl  17652  drsbn0  18374  subgss  19167  symgfixelsi  19477  psgnunilem5  19536  pgpgrp  19636  slwsubg  19652  efgs1b  19778  efgsp1  19779  efgsres  19780  efgredeu  19794  efgred2  19795  efgcpbllemb  19797  rngmgp  20183  srgmgp  20218  ringmgp  20266  irrednu  20451  sdrgsubrg  20814  fldsdrgfld  20821  sdrgint  20827  primefld  20828  primefld0cl  20829  primefld1cl  20830  lmodring  20888  lmodprop2d  20944  lssn0  20961  phlsrng  21672  ocvss  21711  obsss  21767  locfinbas  23551  fclsfil  24039  tmdtps  24105  tgptmd  24108  trgring  24200  tdrgdrng  24203  ngpms  24634  icopnfcnv  24992  xrhmeo  24996  oprpiece1res2  25002  phtpcer  25046  pcoval2  25068  pcoass  25076  clmsca  25117  cphsqrtcl  25237  bncms  25397  itg2ge0  25790  uc1pn0  26205  mon1pn0  26206  sinq12ge0  26568  cosq14gt0  26570  cosq14ge0  26571  cos02pilt1  26586  cosq34lt1  26587  sinord  26594  recosf1o  26595  resinf1o  26596  logrnaddcl  26634  logbcl  26828  relogbreexp  26836  atanf  26941  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  dvatan  26996  areambl  27019  rlimcnp  27026  emgt0  27068  harmoniclbnd  27070  harmonicbnd4  27072  lgamgulmlem2  27091  gausslemma2dlem1a  27427  2sqlem2  27480  2sqlem3  27482  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  logdivbnd  27618  pntpbnd2  27649  pnt  27676  brbtwn2  28938  ax5seglem3  28964  ax5seglem6  28967  axpaschlem  28973  axcontlem2  28998  axcontlem4  29000  crctcshwlkn0lem4  29846  wwlkbp  29874  clwwisshclwwslem  30046  hst1a  32250  stge0  32256  sthil  32266  neldifpr1  32561  f1mptrn  32654  cshwrnid  32928  fsumrp0cl  33007  omndtos  33055  fzo0pmtrlast  33085  wrdpmtrlast  33086  psgnfzto1stlem  33093  slmdsrg  33186  primefldchr  33268  fldgensdrg  33281  primefldgen1  33288  orngogrp  33296  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  elunitge0  33845  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iifiso  33881  rrextnlm  33949  rrextchr  33950  0elros  34134  0elsros  34141  voliune  34193  volfiniune  34194  bnj563  34719  bnj1212  34775  bnj1219  34776  bnj1366  34805  bnj1379  34806  bnj545  34871  bnj594  34888  bnj1118  34960  bnj1177  34982  bnj1190  34984  bnj1398  35010  bnj1417  35017  bnj1450  35026  bnj1312  35034  bnj1523  35047  pthhashvtx  35095  msrval  35506  mclsppslem  35551  dfon2lem1  35747  dfrdg2  35759  cntotbnd  37756  heiborlem5  37775  heiborlem6  37776  eqvrelsymrel  38555  atl0dm  39258  dalem-ccly  39642  stoweidlem60  45981  fourierdlem40  46068  fourierdlem78  46105  uspgrimprop  47757  usgrgrtrirex  47799  ackval40  48427