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

Theorem simp3bi 1141
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1 (𝜑 ↔ (𝜓𝜒𝜃))
Assertion
Ref Expression
simp3bi (𝜑𝜃)

Proof of Theorem simp3bi
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 217 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp3d 1138 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1081
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 1083
This theorem is referenced by:  limuni  6249  smores2  7982  ersym  8291  ertr  8294  fvixp  8455  undifixp  8487  fiint  8784  winalim2  10107  inar1  10186  supmullem1  11600  supmullem2  11601  supmul  11602  eluzle  12245  ico01fl0  13179  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  sin01gt0  15533  divalglem6  15739  gznegcl  16261  gzcjcl  16262  gzaddcl  16263  gzmulcl  16264  gzabssqcl  16267  4sqlem4a  16277  prdsbasprj  16735  xpsff1o  16830  mreintcl  16856  drsdir  17535  subggrp  18212  pmtrfconj  18514  symggen  18518  psgnunilem1  18541  subgpgp  18642  slwispgp  18656  sylow2alem1  18662  oppglsm  18687  efgsdmi  18778  efgsrel  18780  efgsp1  18783  efgsres  18784  efgcpbllemb  18801  efgcpbl  18802  srgi  19181  srgrz  19196  srglz  19197  ringi  19230  ringsrg  19259  irredmul  19379  sdrgint  19503  primefld  19504  lmodlema  19559  lsscl  19634  phllmhm  20692  ipcj  20694  ipeq0  20698  ocvi  20729  obsip  20781  obsocv  20786  2ndcctbss  21979  locfinnei  22047  fclssscls  22542  tmdcn  22607  tgpinv  22609  trgtmd  22688  tdrgunit  22690  ngpds  23128  nrmtngdist  23181  elii1  23454  elii2  23455  icopnfcnv  23461  icopnfhmeo  23462  iccpnfhmeo  23464  xrhmeo  23465  phtpcer  23514  pcoass  23543  clmsubrg  23585  cphnmfval  23711  bnsca  23857  uc1pldg  24657  mon1pldg  24658  sinq12ge0  25009  cosq14gt0  25011  cosq14ge0  25012  sinord  25031  recosf1o  25032  resinf1o  25033  logrnaddcl  25071  logimul  25110  dvlog2lem  25148  atanf  25371  atanneg  25398  atancj  25401  efiatan  25403  atanlogaddlem  25404  atanlogadd  25405  atanlogsub  25407  efiatan2  25408  2efiatan  25409  ressatans  25425  dvatan  25426  areaf  25453  harmonicubnd  25501  harmonicbnd4  25502  lgamgulmlem2  25521  2sqlem2  25908  2sqlem3  25910  dchrvmasumiflem1  25991  pntpbnd2  26077  f1otrg  26571  f1otrge  26572  brbtwn2  26605  ax5seglem3  26631  axpaschlem  26640  axcontlem7  26670  hstel2  29910  stle1  29916  stj  29926  neldifpr2  30208  xrge0adddir  30593  omndadd  30621  slmdlema  30745  lmodslmd  30746  orngmul  30790  xrge0iifcnv  31062  xrge0iifiso  31064  xrge0iifhom  31066  rrextcusp  31132  rrextust  31135  unelros  31316  difelros  31317  inelsros  31323  diffiunisros  31324  sibfinima  31483  eulerpartlemf  31514  eulerpartlemgvv  31520  bnj563  31900  bnj1366  31987  bnj1379  31988  bnj554  32057  bnj557  32059  bnj570  32063  bnj594  32070  bnj1001  32116  bnj1006  32117  bnj1097  32137  bnj1177  32162  bnj1388  32189  bnj1398  32190  bnj1450  32206  bnj1501  32223  bnj1523  32227  pthhashvtx  32258  snmlflim  32463  msrval  32669  mclsssvlem  32693  mclsind  32701  ptrecube  34759  cntotbnd  34942  heiborlem8  34964  dmnnzd  35221  eqvreltrrel  35702  atlex  36319  kelac1  39528  binomcxplemcvg  40551  binomcxplemnotnn0  40553  elixpconstg  41220  fvixp2  41326  stoweidlem39  42190  stoweidlem60  42211  fourierdlem40  42298  fourierdlem78  42335  isringrng  43984
  Copyright terms: Public domain W3C validator