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

Theorem simp2bi 1141
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
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 206 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 1138 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:  smodm  7618  erdm  7923  ixpfn  8082  winafp  9731  inar1  9809  inatsk  9812  tskuni  9817  grur1  9854  supmullem1  11205  supmullem2  11206  supmul  11207  eluzelz  11909  elfz3nn0  12647  elfzo0l  12772  ico01fl0  12834  addmodlteq  12959  cshco  13802  swrds2  13905  ef01bndlem  15133  sin01bnd  15134  cos01bnd  15135  sin01gt0  15139  bitsss  15370  smueqlem  15434  gznegcl  15861  gzcjcl  15862  gzaddcl  15863  gzmulcl  15864  gzabssqcl  15867  4sqlem4a  15877  cshwshashlem2  16025  structn0fun  16091  xpsff1o  16450  mre1cl  16476  drsbn0  17158  subgss  17816  symgfixelsi  18075  psgnunilem5  18134  pgpgrp  18229  slwsubg  18245  efgs1b  18369  efgsp1  18370  efgsres  18371  efgredeu  18385  efgred2  18386  efgcpbllemb  18388  srgmgp  18730  ringmgp  18773  irrednu  18925  lmodring  19093  lmodprop2d  19147  lssn0  19163  phlsrng  20198  ocvss  20236  obsss  20290  locfinbas  21547  fclsfil  22035  tmdtps  22101  tgptmd  22104  trgring  22195  tdrgdrng  22198  ngpms  22625  icopnfcnv  22962  xrhmeo  22966  oprpiece1res2  22972  phtpcer  23015  pcoval2  23036  pcoass  23044  clmsca  23085  cphsqrtcl  23204  bncms  23361  itg2ge0  23721  uc1pn0  24124  mon1pn0  24125  sinq12ge0  24480  cosq14gt0  24482  cosq14ge0  24483  sinord  24500  recosf1o  24501  resinf1o  24502  logrnaddcl  24541  logbcl  24725  relogbreexp  24733  atanf  24827  atanneg  24854  atancj  24857  efiatan  24859  atanlogaddlem  24860  atanlogadd  24861  atanlogsub  24863  efiatan2  24864  2efiatan  24865  tanatan  24866  dvatan  24882  areambl  24905  rlimcnp  24912  emgt0  24953  harmoniclbnd  24955  harmonicbnd4  24957  lgamgulmlem2  24976  gausslemma2dlem1a  25310  2sqlem2  25363  2sqlem3  25365  dchrvmasumlem2  25407  dchrvmasumiflem1  25410  logdivbnd  25465  pntpbnd2  25496  pnt  25523  brbtwn2  26005  ax5seglem3  26031  ax5seglem6  26034  axpaschlem  26040  axcontlem2  26065  axcontlem4  26067  eengbas  26081  ebtwntg  26082  ecgrtg  26083  elntg  26084  crctcshwlkn0lem4  26937  wwlkbp  26965  clwwisshclwwslem  27158  hst1a  29407  stge0  29413  sthil  29423  f1mptrn  29765  fsumrp0cl  30025  omndtos  30035  slmdsrg  30090  orngogrp  30131  psgnfzto1stlem  30180  elunitge0  30275  xrge0iifcnv  30309  xrge0iifcv  30310  xrge0iifiso  30311  rrextnlm  30377  rrextchr  30378  0elros  30563  0elsros  30570  voliune  30622  volfiniune  30623  bnj563  31141  bnj1212  31198  bnj1219  31199  bnj1366  31228  bnj1379  31229  bnj545  31293  bnj594  31310  bnj1118  31380  bnj1177  31402  bnj1190  31404  bnj1398  31430  bnj1417  31437  bnj1450  31446  bnj1312  31454  bnj1523  31467  msrval  31763  mclsppslem  31808  dfon2lem1  32014  dfrdg2  32027  cntotbnd  33926  heiborlem5  33945  heiborlem6  33946  atl0dm  35110  dalem-ccly  35492  elixpconstg  39783  stoweidlem60  40798  fourierdlem40  40885  fourierdlem78  40922  rngmgp  42406
  Copyright terms: Public domain W3C validator