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

Theorem simp3bi 1142
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 206 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp3d 1139 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1072
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 1074
This theorem is referenced by:  limuni  5946  smores2  7621  ersym  7925  ertr  7928  fvixp  8081  undifixp  8112  fiint  8404  winalim2  9730  inar1  9809  supmullem1  11205  supmullem2  11206  supmul  11207  eluzle  11912  ico01fl0  12834  ef01bndlem  15133  sin01bnd  15134  cos01bnd  15135  sin01gt0  15139  divalglem6  15343  gznegcl  15861  gzcjcl  15862  gzaddcl  15863  gzmulcl  15864  gzabssqcl  15867  4sqlem4a  15877  prdsbasprj  16354  xpsff1o  16450  mreintcl  16477  drsdir  17156  subggrp  17818  pmtrfconj  18106  symggen  18110  psgnunilem1  18133  subgpgp  18232  slwispgp  18246  sylow2alem1  18252  oppglsm  18277  efgsdmi  18365  efgsrel  18367  efgsp1  18370  efgsres  18371  efgcpbllemb  18388  efgcpbl  18389  srgi  18731  srgrz  18746  srglz  18747  ringi  18780  ringsrg  18809  irredmul  18929  lmodlema  19090  lsscl  19165  phllmhm  20199  ipcj  20201  ipeq0  20205  ocvi  20235  obsip  20287  obsocv  20292  2ndcctbss  21480  locfinnei  21548  fclssscls  22043  tmdcn  22108  tgpinv  22110  trgtmd  22189  tdrgunit  22191  ngpds  22629  nrmtngdist  22682  elii1  22955  elii2  22956  icopnfcnv  22962  icopnfhmeo  22963  iccpnfhmeo  22965  xrhmeo  22966  phtpcer  23015  pcoass  23044  clmsubrg  23086  cphnmfval  23212  bnsca  23356  uc1pldg  24127  mon1pldg  24128  sinq12ge0  24480  cosq14gt0  24482  cosq14ge0  24483  sinord  24500  recosf1o  24501  resinf1o  24502  logrnaddcl  24541  logimul  24580  dvlog2lem  24618  atanf  24827  atanneg  24854  atancj  24857  efiatan  24859  atanlogaddlem  24860  atanlogadd  24861  atanlogsub  24863  efiatan2  24864  2efiatan  24865  ressatans  24881  dvatan  24882  areaf  24908  harmonicubnd  24956  harmonicbnd4  24957  lgamgulmlem2  24976  2sqlem2  25363  2sqlem3  25365  dchrvmasumiflem1  25410  pntpbnd2  25496  f1otrg  25971  f1otrge  25972  brbtwn2  26005  ax5seglem3  26031  axpaschlem  26040  axcontlem7  26070  hstel2  29408  stle1  29414  stj  29424  xrge0adddir  30022  omndadd  30036  slmdlema  30086  lmodslmd  30087  orngmul  30133  xrge0iifcnv  30309  xrge0iifiso  30311  xrge0iifhom  30313  rrextcusp  30379  rrextust  30382  unelros  30564  difelros  30565  inelsros  30571  diffiunisros  30572  sibfinima  30731  eulerpartlemf  30762  eulerpartlemgvv  30768  bnj563  31141  bnj1366  31228  bnj1379  31229  bnj554  31297  bnj557  31299  bnj570  31303  bnj594  31310  bnj1001  31356  bnj1006  31357  bnj1097  31377  bnj1177  31402  bnj1388  31429  bnj1398  31430  bnj1450  31446  bnj1501  31463  bnj1523  31467  snmlflim  31642  msrval  31763  mclsssvlem  31787  mclsind  31795  ptrecube  33740  cntotbnd  33926  heiborlem8  33948  dmnnzd  34205  atlex  35124  kelac1  38153  binomcxplemcvg  39073  binomcxplemnotnn0  39075  elixpconstg  39783  fvixp2  39906  stoweidlem39  40777  stoweidlem60  40798  fourierdlem40  40885  fourierdlem78  40922  isringrng  42409
  Copyright terms: Public domain W3C validator