MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1bi Structured version   Visualization version   GIF version

Theorem simp1bi 1139
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1 (𝜑 ↔ (𝜓𝜒𝜃))
Assertion
Ref Expression
simp1bi (𝜑𝜓)

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 206 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 1136 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  limord  5926  smores2  7607  smofvon2  7609  smofvon  7612  errel  7908  lincmb01cmp  12521  iccf1o  12522  elfznn0  12639  elfzouz  12681  ef01bndlem  15119  sin01bnd  15120  cos01bnd  15121  sin01gt0  15125  cos01gt0  15126  sin02gt0  15127  gzcn  15842  mresspw  16459  drsprs  17143  ipodrscl  17369  subgrcl  17806  pmtrfconj  18092  pgpprm  18214  slwprm  18230  efgsdmi  18351  efgsrel  18353  efgs1b  18355  efgsp1  18356  efgsres  18357  efgsfo  18358  efgredlema  18359  efgredlemf  18360  efgredlemd  18363  efgredlemc  18364  efgredlem  18366  efgrelexlemb  18369  efgcpbllemb  18374  srgcmn  18715  ringgrp  18759  irredcl  18911  lmodgrp  19079  lssss  19146  phllvec  20190  obsrcl  20283  locfintop  21544  fclstop  22034  tmdmnd  22098  tgpgrp  22101  trgtgp  22190  tdrgtrg  22195  ust0  22242  ngpgrp  22622  elii1  22953  elii2  22954  icopnfcnv  22960  icopnfhmeo  22961  iccpnfhmeo  22963  xrhmeo  22964  oprpiece1res1  22969  oprpiece1res2  22970  phtpcer  23013  pcoval2  23034  pcoass  23042  clmlmod  23085  cphphl  23189  cphnlm  23190  cphsca  23197  bnnvc  23355  uc1pcl  24122  mon1pcl  24123  sinq12ge0  24480  cosq14ge0  24483  cosord  24498  cos11  24499  recosf1o  24501  resinf1o  24502  efifo  24513  logrncn  24529  atanf  24827  atanneg  24854  efiatan  24859  atanlogaddlem  24860  atanlogadd  24861  atanlogsub  24863  efiatan2  24864  2efiatan  24865  tanatan  24866  areass  24906  dchrvmasumlem2  25407  dchrvmasumiflem1  25410  brbtwn2  26005  ax5seglem1  26028  ax5seglem2  26029  ax5seglem3  26031  ax5seglem5  26033  ax5seglem6  26034  ax5seglem9  26037  ax5seg  26038  axbtwnid  26039  axpaschlem  26040  axpasch  26041  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  pthistrl  26855  clwwlkbp  27134  sticl  29413  hstcl  29415  omndmnd  30043  slmdcmn  30097  orngring  30139  elunitrn  30282  rrextnrg  30384  rrextdrg  30385  rossspw  30571  srossspw  30578  eulerpartlemd  30767  eulerpartlemf  30771  eulerpartlemgvv  30777  eulerpartlemgu  30778  eulerpartlemgh  30779  eulerpartlemgs2  30781  eulerpartlemn  30782  bnj564  31151  bnj1366  31237  bnj545  31302  bnj548  31304  bnj558  31309  bnj570  31312  bnj580  31320  bnj929  31343  bnj998  31363  bnj1006  31366  bnj1190  31413  bnj1523  31476  msrval  31772  mthmpps  31816  atllat  35108  stoweidlem60  40791  fourierdlem111  40948  rngabl  42402
  Copyright terms: Public domain W3C validator