Theorem simp2bi 1137

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  smodm  7831  erdm  8140  ixpfn  8306  winafp  9954  inar1  10032  inatsk  10035  tskuni  10040  grur1  10077  supmullem1  11448  supmullem2  11449  supmul  11450  eluzelz  12092  elfz3nn0  12840  elfzo0l  12965  ico01fl0  13027  addmodlteq  13152  cshco  14022  swrds2  14126  ef01bndlem  15358  sin01bnd  15359  cos01bnd  15360  sin01gt0  15364  bitsss  15596  smueqlem  15660  gznegcl  16088  gzcjcl  16089  gzaddcl  16090  gzmulcl  16091  gzabssqcl  16094  4sqlem4a  16104  cshwshashlem2  16247  structn0fun  16312  xpsff1o  16657  mre1cl  16682  drsbn0  17364  subgss  18022  symgfixelsi  18282  psgnunilem5  18341  pgpgrp  18437  slwsubg  18453  efgs1b  18577  efgsp1  18578  efgsres  18579  efgredeu  18593  efgred2  18594  efgcpbllemb  18596  srgmgp  18938  ringmgp  18981  irrednu  19133  sdrgint  19261  primefld  19262  primefld0cl  19263  primefld1cl  19264  lmodring  19320  lmodprop2d  19374  lssn0  19390  phlsrng  20445  ocvss  20484  obsss  20538  locfinbas  21802  fclsfil  22290  tmdtps  22356  tgptmd  22359  trgring  22450  tdrgdrng  22453  ngpms  22880  icopnfcnv  23217  xrhmeo  23221  oprpiece1res2  23227  phtpcer  23270  pcoval2  23291  pcoass  23299  clmsca  23340  cphsqrtcl  23459  bncms  23618  itg2ge0  24007  uc1pn0  24410  mon1pn0  24411  sinq12ge0  24765  cosq14gt0  24767  cosq14ge0  24768  sinord  24787  recosf1o  24788  resinf1o  24789  logrnaddcl  24827  logbcl  25014  relogbreexp  25022  atanf  25127  atanneg  25154  atancj  25157  efiatan  25159  atanlogaddlem  25160  atanlogadd  25161  atanlogsub  25163  efiatan2  25164  2efiatan  25165  tanatan  25166  dvatan  25182  areambl  25206  rlimcnp  25213  emgt0  25254  harmoniclbnd  25256  harmonicbnd4  25258  lgamgulmlem2  25277  gausslemma2dlem1a  25611  2sqlem2  25664  2sqlem3  25666  dchrvmasumlem2  25744  dchrvmasumiflem1  25747  logdivbnd  25802  pntpbnd2  25833  pnt  25860  brbtwn2  26362  ax5seglem3  26388  ax5seglem6  26391  axpaschlem  26397  axcontlem2  26422  axcontlem4  26424  crctcshwlkn0lem4  27266  wwlkbp  27294  clwwisshclwwslem  27467  hst1a  29674  stge0  29680  sthil  29690  f1mptrn  30043  cshwrnid  30279  fsumrp0cl  30326  omndtos  30336  slmdsrg  30431  primefldchr  30476  orngogrp  30483  psgnfzto1stlem  30620  elunitge0  30715  xrge0iifcnv  30749  xrge0iifcv  30750  xrge0iifiso  30751  rrextnlm  30817  rrextchr  30818  0elros  31002  0elsros  31009  voliune  31061  volfiniune  31062  bnj563  31587  bnj1212  31644  bnj1219  31645  bnj1366  31674  bnj1379  31675  bnj545  31739  bnj594  31756  bnj1118  31826  bnj1177  31848  bnj1190  31850  bnj1398  31876  bnj1417  31883  bnj1450  31892  bnj1312  31900  bnj1523  31913  pthhashvtx  31938  msrval  32338  mclsppslem  32383  dfon2lem1  32581  dfrdg2  32594  cntotbnd  34552  heiborlem5  34571  heiborlem6  34572  eqvrelsymrel  35315  atl0dm  35919  dalem-ccly  36302  stoweidlem60  41841  fourierdlem40  41928  fourierdlem78  41965  rngmgp  43581