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

Theorem simp1bi 1140
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 1137 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  limord  5945  smores2  7620  smofvon2  7622  smofvon  7625  errel  7920  lincmb01cmp  12508  iccf1o  12509  elfznn0  12626  elfzouz  12668  ef01bndlem  15113  sin01bnd  15114  cos01bnd  15115  sin01gt0  15119  cos01gt0  15120  sin02gt0  15121  gzcn  15838  mresspw  16454  drsprs  17137  ipodrscl  17363  subgrcl  17800  pmtrfconj  18086  pgpprm  18208  slwprm  18224  efgsdmi  18345  efgsrel  18347  efgs1b  18349  efgsp1  18350  efgsres  18351  efgsfo  18352  efgredlema  18353  efgredlemf  18354  efgredlemd  18357  efgredlemc  18358  efgredlem  18360  efgrelexlemb  18363  efgcpbllemb  18368  srgcmn  18708  ringgrp  18752  irredcl  18904  lmodgrp  19072  lssss  19139  phllvec  20176  obsrcl  20269  locfintop  21526  fclstop  22016  tmdmnd  22080  tgpgrp  22083  trgtgp  22172  tdrgtrg  22177  ust0  22224  ngpgrp  22604  elii1  22935  elii2  22936  icopnfcnv  22942  icopnfhmeo  22943  iccpnfhmeo  22945  xrhmeo  22946  oprpiece1res1  22951  oprpiece1res2  22952  phtpcer  22995  pcoval2  23016  pcoass  23024  clmlmod  23067  cphphl  23171  cphnlm  23172  cphsca  23179  bnnvc  23337  uc1pcl  24102  mon1pcl  24103  sinq12ge0  24459  cosq14ge0  24462  cosord  24477  cos11  24478  recosf1o  24480  resinf1o  24481  efifo  24492  logrncn  24508  atanf  24806  atanneg  24833  efiatan  24838  atanlogaddlem  24839  atanlogadd  24840  atanlogsub  24842  efiatan2  24843  2efiatan  24844  tanatan  24845  areass  24885  dchrvmasumlem2  25386  dchrvmasumiflem1  25389  brbtwn2  25984  ax5seglem1  26007  ax5seglem2  26008  ax5seglem3  26010  ax5seglem5  26012  ax5seglem6  26013  ax5seglem9  26016  ax5seg  26017  axbtwnid  26018  axpaschlem  26019  axpasch  26020  axcontlem2  26044  axcontlem4  26046  axcontlem7  26049  pthistrl  26831  clwwlkbp  27108  sticl  29383  hstcl  29385  omndmnd  30013  slmdcmn  30067  orngring  30109  elunitrn  30252  rrextnrg  30354  rrextdrg  30355  rossspw  30541  srossspw  30548  eulerpartlemd  30737  eulerpartlemf  30741  eulerpartlemgvv  30747  eulerpartlemgu  30748  eulerpartlemgh  30749  eulerpartlemgs2  30751  eulerpartlemn  30752  bnj564  31121  bnj1366  31207  bnj545  31272  bnj548  31274  bnj558  31279  bnj570  31282  bnj580  31290  bnj929  31313  bnj998  31333  bnj1006  31336  bnj1190  31383  bnj1523  31446  msrval  31742  mthmpps  31786  atllat  35090  stoweidlem60  40780  fourierdlem111  40937  rngabl  42387
  Copyright terms: Public domain W3C validator