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

Theorem simp2bi 1097
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 1094 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1054
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 1056
This theorem is referenced by:  smodm  7493  erdm  7797  ixpfn  7956  winafp  9557  inar1  9635  inatsk  9638  tskuni  9643  grur1  9680  supmullem1  11031  supmullem2  11032  supmul  11033  eluzelz  11735  elfz3nn0  12472  elfzo0l  12598  ico01fl0  12660  addmodlteq  12785  cshco  13628  swrds2  13731  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  sin01gt0  14964  bitsss  15195  smueqlem  15259  gznegcl  15686  gzcjcl  15687  gzaddcl  15688  gzmulcl  15689  gzabssqcl  15692  4sqlem4a  15702  cshwshashlem2  15850  structn0fun  15916  xpsff1o  16275  mre1cl  16301  drsbn0  16984  subgss  17642  symgfixelsi  17901  psgnunilem5  17960  pgpgrp  18055  slwsubg  18071  efgs1b  18195  efgsp1  18196  efgsres  18197  efgredeu  18211  efgred2  18212  efgcpbllemb  18214  srgmgp  18556  ringmgp  18599  irrednu  18751  lmodring  18919  lmodprop2d  18973  lssn0  18989  phlsrng  20024  ocvss  20062  obsss  20116  locfinbas  21373  fclsfil  21861  tmdtps  21927  tgptmd  21930  trgring  22021  tdrgdrng  22024  ngpms  22451  icopnfcnv  22788  xrhmeo  22792  oprpiece1res2  22798  phtpcer  22841  pcoval2  22862  pcoass  22870  clmsca  22911  cphsqrtcl  23030  bncms  23187  itg2ge0  23547  uc1pn0  23950  mon1pn0  23951  sinq12ge0  24305  cosq14gt0  24307  cosq14ge0  24308  sinord  24325  recosf1o  24326  resinf1o  24327  logrnaddcl  24366  logbcl  24550  relogbreexp  24558  atanf  24652  atanneg  24679  atancj  24682  efiatan  24684  atanlogaddlem  24685  atanlogadd  24686  atanlogsub  24688  efiatan2  24689  2efiatan  24690  tanatan  24691  dvatan  24707  areambl  24730  rlimcnp  24737  emgt0  24778  harmoniclbnd  24780  harmonicbnd4  24782  lgamgulmlem2  24801  gausslemma2dlem1a  25135  2sqlem2  25188  2sqlem3  25190  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  logdivbnd  25290  pntpbnd2  25321  pnt  25348  brbtwn2  25830  ax5seglem3  25856  ax5seglem6  25859  axpaschlem  25865  axcontlem2  25890  axcontlem4  25892  eengbas  25906  ebtwntg  25907  ecgrtg  25908  elntg  25909  crctcshwlkn0lem4  26761  wwlkbp  26789  clwwisshclwwslem  26971  hst1a  29205  stge0  29211  sthil  29221  f1mptrn  29563  fsumrp0cl  29823  omndtos  29833  slmdsrg  29888  orngogrp  29929  psgnfzto1stlem  29978  elunitge0  30073  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iifiso  30109  rrextnlm  30175  rrextchr  30176  0elros  30361  0elsros  30368  voliune  30420  volfiniune  30421  bnj563  30939  bnj1212  30996  bnj1219  30997  bnj1366  31026  bnj1379  31027  bnj545  31091  bnj594  31108  bnj1118  31178  bnj1177  31200  bnj1190  31202  bnj1398  31228  bnj1417  31235  bnj1450  31244  bnj1312  31252  bnj1523  31265  msrval  31561  mclsppslem  31606  dfon2lem1  31812  dfrdg2  31825  cntotbnd  33725  heiborlem5  33744  heiborlem6  33745  atl0dm  34907  dalem-ccly  35289  elixpconstg  39580  stoweidlem60  40595  fourierdlem40  40682  fourierdlem78  40719  rngmgp  42203
  Copyright terms: Public domain W3C validator