Theorem simp2bi 1144

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  smodm  8153  erdm  8466  ixpfn  8649  winafp  10384  inar1  10462  inatsk  10465  tskuni  10470  grur1  10507  supmullem1  11875  supmullem2  11876  supmul  11877  eluzelz  12521  elfz3nn0  13279  elfzo0l  13405  ico01fl0  13467  addmodlteq  13594  cshco  14477  swrds2  14581  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  bitsss  16061  smueqlem  16125  gznegcl  16564  gzcjcl  16565  gzaddcl  16566  gzmulcl  16567  gzabssqcl  16570  4sqlem4a  16580  cshwshashlem2  16726  structn0fun  16780  xpsff1o  17195  mre1cl  17220  drsbn0  17937  subgss  18671  symgfixelsi  18958  psgnunilem5  19017  pgpgrp  19114  slwsubg  19130  efgs1b  19257  efgsp1  19258  efgsres  19259  efgredeu  19273  efgred2  19274  efgcpbllemb  19276  srgmgp  19661  ringmgp  19704  irrednu  19862  sdrgint  19987  primefld  19988  primefld0cl  19989  primefld1cl  19990  lmodring  20046  lmodprop2d  20100  lssn0  20117  phlsrng  20748  ocvss  20787  obsss  20841  locfinbas  22581  fclsfil  23069  tmdtps  23135  tgptmd  23138  trgring  23230  tdrgdrng  23233  ngpms  23662  icopnfcnv  24011  xrhmeo  24015  oprpiece1res2  24021  phtpcer  24064  pcoval2  24085  pcoass  24093  clmsca  24134  cphsqrtcl  24253  bncms  24413  itg2ge0  24805  uc1pn0  25215  mon1pn0  25216  sinq12ge0  25570  cosq14gt0  25572  cosq14ge0  25573  cos02pilt1  25587  cosq34lt1  25588  sinord  25595  recosf1o  25596  resinf1o  25597  logrnaddcl  25635  logbcl  25822  relogbreexp  25830  atanf  25935  atanneg  25962  atancj  25965  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsub  25971  efiatan2  25972  2efiatan  25973  tanatan  25974  dvatan  25990  areambl  26013  rlimcnp  26020  emgt0  26061  harmoniclbnd  26063  harmonicbnd4  26065  lgamgulmlem2  26084  gausslemma2dlem1a  26418  2sqlem2  26471  2sqlem3  26473  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  logdivbnd  26609  pntpbnd2  26640  pnt  26667  brbtwn2  27176  ax5seglem3  27202  ax5seglem6  27205  axpaschlem  27211  axcontlem2  27236  axcontlem4  27238  crctcshwlkn0lem4  28079  wwlkbp  28107  clwwisshclwwslem  28279  hst1a  30481  stge0  30487  sthil  30497  neldifpr1  30782  f1mptrn  30871  cshwrnid  31135  fsumrp0cl  31206  omndtos  31233  psgnfzto1stlem  31269  slmdsrg  31362  primefldchr  31395  orngogrp  31402  elunitge0  31751  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iifiso  31787  rrextnlm  31853  rrextchr  31854  0elros  32038  0elsros  32045  voliune  32097  volfiniune  32098  bnj563  32623  bnj1212  32679  bnj1219  32680  bnj1366  32709  bnj1379  32710  bnj545  32775  bnj594  32792  bnj1118  32864  bnj1177  32886  bnj1190  32888  bnj1398  32914  bnj1417  32921  bnj1450  32930  bnj1312  32938  bnj1523  32951  pthhashvtx  32989  msrval  33400  mclsppslem  33445  dfon2lem1  33665  dfrdg2  33677  cntotbnd  35881  heiborlem5  35900  heiborlem6  35901  eqvrelsymrel  36639  atl0dm  37243  dalem-ccly  37626  stoweidlem60  43491  fourierdlem40  43578  fourierdlem78  43615  rngmgp  45324  ackval40  45927