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

Theorem simp2bi 1147
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 215 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 1144 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  smodm  8298  erdm  8661  ixpfn  8844  winafp  10638  inar1  10716  inatsk  10719  tskuni  10724  grur1  10761  supmullem1  12130  supmullem2  12131  supmul  12132  eluzelz  12778  elfz3nn0  13541  elfzo0l  13668  ico01fl0  13730  addmodlteq  13857  cshco  14731  swrds2  14835  ef01bndlem  16071  sin01bnd  16072  cos01bnd  16073  sin01gt0  16077  bitsss  16311  smueqlem  16375  gznegcl  16812  gzcjcl  16813  gzaddcl  16814  gzmulcl  16815  gzabssqcl  16818  4sqlem4a  16828  cshwshashlem2  16974  structn0fun  17028  xpsff1o  17454  mre1cl  17479  drsbn0  18198  subgss  18934  symgfixelsi  19222  psgnunilem5  19281  pgpgrp  19381  slwsubg  19397  efgs1b  19523  efgsp1  19524  efgsres  19525  efgredeu  19539  efgred2  19540  efgcpbllemb  19542  srgmgp  19927  ringmgp  19975  irrednu  20141  fldsdrgfld  20279  sdrgint  20285  primefld  20286  primefld0cl  20287  primefld1cl  20288  lmodring  20344  lmodprop2d  20399  lssn0  20416  phlsrng  21051  ocvss  21090  obsss  21146  locfinbas  22889  fclsfil  23377  tmdtps  23443  tgptmd  23446  trgring  23538  tdrgdrng  23541  ngpms  23972  icopnfcnv  24321  xrhmeo  24325  oprpiece1res2  24331  phtpcer  24374  pcoval2  24395  pcoass  24403  clmsca  24444  cphsqrtcl  24564  bncms  24724  itg2ge0  25116  uc1pn0  25526  mon1pn0  25527  sinq12ge0  25881  cosq14gt0  25883  cosq14ge0  25884  cos02pilt1  25898  cosq34lt1  25899  sinord  25906  recosf1o  25907  resinf1o  25908  logrnaddcl  25946  logbcl  26133  relogbreexp  26141  atanf  26246  atanneg  26273  atancj  26276  efiatan  26278  atanlogaddlem  26279  atanlogadd  26280  atanlogsub  26282  efiatan2  26283  2efiatan  26284  tanatan  26285  dvatan  26301  areambl  26324  rlimcnp  26331  emgt0  26372  harmoniclbnd  26374  harmonicbnd4  26376  lgamgulmlem2  26395  gausslemma2dlem1a  26729  2sqlem2  26782  2sqlem3  26784  dchrvmasumlem2  26862  dchrvmasumiflem1  26865  logdivbnd  26920  pntpbnd2  26951  pnt  26978  brbtwn2  27896  ax5seglem3  27922  ax5seglem6  27925  axpaschlem  27931  axcontlem2  27956  axcontlem4  27958  crctcshwlkn0lem4  28800  wwlkbp  28828  clwwisshclwwslem  29000  hst1a  31202  stge0  31208  sthil  31218  neldifpr1  31503  f1mptrn  31595  cshwrnid  31864  fsumrp0cl  31935  omndtos  31962  psgnfzto1stlem  31998  slmdsrg  32091  primefldchr  32125  fldgensdrg  32130  primefldgen1  32135  orngogrp  32143  elunitge0  32537  xrge0iifcnv  32571  xrge0iifcv  32572  xrge0iifiso  32573  rrextnlm  32641  rrextchr  32642  0elros  32826  0elsros  32833  voliune  32885  volfiniune  32886  bnj563  33412  bnj1212  33468  bnj1219  33469  bnj1366  33498  bnj1379  33499  bnj545  33564  bnj594  33581  bnj1118  33653  bnj1177  33675  bnj1190  33677  bnj1398  33703  bnj1417  33710  bnj1450  33719  bnj1312  33727  bnj1523  33740  pthhashvtx  33778  msrval  34189  mclsppslem  34234  dfon2lem1  34414  dfrdg2  34426  cntotbnd  36301  heiborlem5  36320  heiborlem6  36321  eqvrelsymrel  37107  atl0dm  37810  dalem-ccly  38194  sdrgsubrg  40759  stoweidlem60  44387  fourierdlem40  44474  fourierdlem78  44511  rngmgp  46262  ackval40  46865
  Copyright terms: Public domain W3C validator