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

Theorem simp2bi 1169
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 207 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp2d 1166 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  smodm  7691  erdm  7996  ixpfn  8158  winafp  9811  inar1  9889  inatsk  9892  tskuni  9897  grur1  9934  supmullem1  11285  supmullem2  11286  supmul  11287  eluzelz  11921  elfz3nn0  12664  elfzo0l  12789  ico01fl0  12851  addmodlteq  12976  cshco  13813  swrds2  13916  ef01bndlem  15141  sin01bnd  15142  cos01bnd  15143  sin01gt0  15147  bitsss  15374  smueqlem  15438  gznegcl  15863  gzcjcl  15864  gzaddcl  15865  gzmulcl  15866  gzabssqcl  15869  4sqlem4a  15879  cshwshashlem2  16022  structn0fun  16087  xpsff1o  16440  mre1cl  16466  drsbn0  17149  subgss  17804  symgfixelsi  18063  psgnunilem5  18122  pgpgrp  18217  slwsubg  18233  efgs1b  18357  efgsp1  18358  efgsres  18359  efgredeu  18373  efgred2  18374  efgcpbllemb  18376  srgmgp  18719  ringmgp  18762  irrednu  18914  lmodring  19082  lmodprop2d  19136  lssn0  19152  phlsrng  20193  ocvss  20232  obsss  20286  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  23362  itg2ge0  23726  uc1pn0  24129  mon1pn0  24130  sinq12ge0  24485  cosq14gt0  24487  cosq14ge0  24488  sinord  24505  recosf1o  24506  resinf1o  24507  logrnaddcl  24545  logbcl  24729  relogbreexp  24737  atanf  24831  atanneg  24858  atancj  24861  efiatan  24863  atanlogaddlem  24864  atanlogadd  24865  atanlogsub  24867  efiatan2  24868  2efiatan  24869  tanatan  24870  dvatan  24886  areambl  24909  rlimcnp  24916  emgt0  24957  harmoniclbnd  24959  harmonicbnd4  24961  lgamgulmlem2  24980  gausslemma2dlem1a  25314  2sqlem2  25367  2sqlem3  25369  dchrvmasumlem2  25411  dchrvmasumiflem1  25414  logdivbnd  25469  pntpbnd2  25500  pnt  25527  brbtwn2  26009  ax5seglem3  26035  ax5seglem6  26038  axpaschlem  26044  axcontlem2  26069  axcontlem4  26071  eengbas  26085  ebtwntg  26086  ecgrtg  26087  elntg  26088  crctcshwlkn0lem4  26944  wwlkbp  26972  clwwisshclwwslem  27167  hst1a  29415  stge0  29421  sthil  29431  f1mptrn  29772  fsumrp0cl  30030  omndtos  30040  slmdsrg  30095  orngogrp  30136  psgnfzto1stlem  30185  elunitge0  30280  xrge0iifcnv  30314  xrge0iifcv  30315  xrge0iifiso  30316  rrextnlm  30382  rrextchr  30383  0elros  30568  0elsros  30575  voliune  30627  volfiniune  30628  bnj563  31145  bnj1212  31202  bnj1219  31203  bnj1366  31232  bnj1379  31233  bnj545  31297  bnj594  31314  bnj1118  31384  bnj1177  31406  bnj1190  31408  bnj1398  31434  bnj1417  31441  bnj1450  31450  bnj1312  31458  bnj1523  31471  msrval  31767  mclsppslem  31812  dfon2lem1  32017  dfrdg2  32030  cntotbnd  33912  heiborlem5  33931  heiborlem6  33932  atl0dm  35088  dalem-ccly  35471  elixpconstg  39764  stoweidlem60  40761  fourierdlem40  40848  fourierdlem78  40885  rngmgp  42451
  Copyright terms: Public domain W3C validator