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

Theorem simp2bi 1075
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 1072 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  smodm  7393  erdm  7697  ixpfn  7858  winafp  9463  inar1  9541  inatsk  9544  tskuni  9549  grur1  9586  supmullem1  10937  supmullem2  10938  supmul  10939  eluzelz  11641  elfz3nn0  12375  elfzo0l  12499  ico01fl0  12560  addmodlteq  12685  cshco  13519  swrds2  13619  ef01bndlem  14839  sin01bnd  14840  cos01bnd  14841  sin01gt0  14845  bitsss  15072  smueqlem  15136  gznegcl  15563  gzcjcl  15564  gzaddcl  15565  gzmulcl  15566  gzabssqcl  15569  4sqlem4a  15579  cshwshashlem2  15727  structn0fun  15792  xpsff1o  16149  mre1cl  16175  drsbn0  16858  subgss  17516  symgfixelsi  17776  psgnunilem5  17835  pgpgrp  17930  slwsubg  17946  efgs1b  18070  efgsp1  18071  efgsres  18072  efgredeu  18086  efgred2  18087  efgcpbllemb  18089  srgmgp  18431  ringmgp  18474  irrednu  18626  lmodring  18792  lmodprop2d  18846  lssn0  18860  phlsrng  19895  ocvss  19933  obsss  19987  locfinbas  21235  fclsfil  21724  tmdtps  21790  tgptmd  21793  trgring  21884  tdrgdrng  21887  ngpms  22314  icopnfcnv  22649  xrhmeo  22653  oprpiece1res2  22659  phtpcer  22702  phtpcerOLD  22703  pcoval2  22724  pcoass  22732  clmsca  22773  cphsqrtcl  22892  bncms  23049  itg2ge0  23408  uc1pn0  23809  mon1pn0  23810  sinq12ge0  24164  cosq14gt0  24166  cosq14ge0  24167  sinord  24184  recosf1o  24185  resinf1o  24186  logrnaddcl  24225  logbcl  24405  relogbreexp  24413  atanf  24507  atanneg  24534  atancj  24537  efiatan  24539  atanlogaddlem  24540  atanlogadd  24541  atanlogsub  24543  efiatan2  24544  2efiatan  24545  tanatan  24546  dvatan  24562  areambl  24585  rlimcnp  24592  emgt0  24633  harmoniclbnd  24635  harmonicbnd4  24637  lgamgulmlem2  24656  gausslemma2dlem1a  24990  2sqlem2  25043  2sqlem3  25045  dchrvmasumlem2  25087  dchrvmasumiflem1  25090  logdivbnd  25145  pntpbnd2  25176  pnt  25203  brbtwn2  25685  ax5seglem3  25711  ax5seglem6  25714  axpaschlem  25720  axcontlem2  25745  axcontlem4  25747  eengbas  25761  ebtwntg  25762  ecgrtg  25763  elntg  25764  crctcshwlkn0lem4  26574  wwlkbp  26601  clwwisshclwwslem  26793  hst1a  28926  stge0  28932  sthil  28942  f1mptrn  29278  fsumrp0cl  29480  omndtos  29490  slmdsrg  29545  orngogrp  29586  psgnfzto1stlem  29635  elunitge0  29727  xrge0iifcnv  29761  xrge0iifcv  29762  xrge0iifiso  29763  rrextnlm  29829  rrextchr  29830  0elros  30014  0elsros  30021  voliune  30073  volfiniune  30074  bnj563  30521  bnj1212  30578  bnj1219  30579  bnj1366  30608  bnj1379  30609  bnj545  30673  bnj594  30690  bnj1118  30760  bnj1177  30782  bnj1190  30784  bnj1398  30810  bnj1417  30817  bnj1450  30826  bnj1312  30834  bnj1523  30847  msrval  31143  mclsppslem  31188  dfon2lem1  31389  dfrdg2  31402  cntotbnd  33227  heiborlem5  33246  heiborlem6  33247  atl0dm  34069  dalem-ccly  34451  elixpconstg  38751  stoweidlem60  39584  fourierdlem40  39671  fourierdlem78  39708  rngmgp  41166
  Copyright terms: Public domain W3C validator