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

Theorem simp2bi 1138
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 217 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 1135 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  smodm  7977  erdm  8288  ixpfn  8455  winafp  10107  inar1  10185  inatsk  10188  tskuni  10193  grur1  10230  supmullem1  11599  supmullem2  11600  supmul  11601  eluzelz  12241  elfz3nn0  12989  elfzo0l  13115  ico01fl0  13177  addmodlteq  13302  cshco  14186  swrds2  14290  ef01bndlem  15525  sin01bnd  15526  cos01bnd  15527  sin01gt0  15531  bitsss  15763  smueqlem  15827  gznegcl  16259  gzcjcl  16260  gzaddcl  16261  gzmulcl  16262  gzabssqcl  16265  4sqlem4a  16275  cshwshashlem2  16418  structn0fun  16483  xpsff1o  16828  mre1cl  16853  drsbn0  17535  subgss  18218  symgfixelsi  18492  psgnunilem5  18551  pgpgrp  18648  slwsubg  18664  efgs1b  18791  efgsp1  18792  efgsres  18793  efgredeu  18807  efgred2  18808  efgcpbllemb  18810  srgmgp  19189  ringmgp  19232  irrednu  19384  sdrgint  19512  primefld  19513  primefld0cl  19514  primefld1cl  19515  lmodring  19571  lmodprop2d  19625  lssn0  19641  phlsrng  20703  ocvss  20742  obsss  20796  locfinbas  22058  fclsfil  22546  tmdtps  22612  tgptmd  22615  trgring  22706  tdrgdrng  22709  ngpms  23136  icopnfcnv  23473  xrhmeo  23477  oprpiece1res2  23483  phtpcer  23526  pcoval2  23547  pcoass  23555  clmsca  23596  cphsqrtcl  23715  bncms  23874  itg2ge0  24263  uc1pn0  24666  mon1pn0  24667  sinq12ge0  25021  cosq14gt0  25023  cosq14ge0  25024  cos02pilt1  25038  cosq34lt1  25039  sinord  25045  recosf1o  25046  resinf1o  25047  logrnaddcl  25085  logbcl  25272  relogbreexp  25280  atanf  25385  atanneg  25412  atancj  25415  efiatan  25417  atanlogaddlem  25418  atanlogadd  25419  atanlogsub  25421  efiatan2  25422  2efiatan  25423  tanatan  25424  dvatan  25440  areambl  25463  rlimcnp  25470  emgt0  25511  harmoniclbnd  25513  harmonicbnd4  25515  lgamgulmlem2  25534  gausslemma2dlem1a  25868  2sqlem2  25921  2sqlem3  25923  dchrvmasumlem2  26001  dchrvmasumiflem1  26004  logdivbnd  26059  pntpbnd2  26090  pnt  26117  brbtwn2  26618  ax5seglem3  26644  ax5seglem6  26647  axpaschlem  26653  axcontlem2  26678  axcontlem4  26680  crctcshwlkn0lem4  27518  wwlkbp  27546  clwwisshclwwslem  27719  hst1a  29922  stge0  29928  sthil  29938  neldifpr1  30220  f1mptrn  30308  cshwrnid  30562  fsumrp0cl  30609  omndtos  30633  psgnfzto1stlem  30669  slmdsrg  30762  primefldchr  30794  orngogrp  30801  elunitge0  31041  xrge0iifcnv  31075  xrge0iifcv  31076  xrge0iifiso  31077  rrextnlm  31143  rrextchr  31144  0elros  31328  0elsros  31335  voliune  31387  volfiniune  31388  bnj563  31913  bnj1212  31970  bnj1219  31971  bnj1366  32000  bnj1379  32001  bnj545  32066  bnj594  32083  bnj1118  32153  bnj1177  32175  bnj1190  32177  bnj1398  32203  bnj1417  32210  bnj1450  32219  bnj1312  32227  bnj1523  32240  pthhashvtx  32271  msrval  32682  mclsppslem  32727  dfon2lem1  32925  dfrdg2  32937  cntotbnd  34955  heiborlem5  34974  heiborlem6  34975  eqvrelsymrel  35714  atl0dm  36318  dalem-ccly  36701  stoweidlem60  42222  fourierdlem40  42309  fourierdlem78  42346  rngmgp  44077
  Copyright terms: Public domain W3C validator