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

Theorem simp3bi 1098
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 1095 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:  limuni  5823  smores2  7496  ersym  7799  ertr  7802  fvixp  7955  undifixp  7986  fiint  8278  winalim2  9556  inar1  9635  supmullem1  11031  supmullem2  11032  supmul  11033  eluzle  11738  ico01fl0  12660  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  sin01gt0  14964  divalglem6  15168  gznegcl  15686  gzcjcl  15687  gzaddcl  15688  gzmulcl  15689  gzabssqcl  15692  4sqlem4a  15702  prdsbasprj  16179  xpsff1o  16275  mreintcl  16302  drsdir  16982  subggrp  17644  pmtrfconj  17932  symggen  17936  psgnunilem1  17959  subgpgp  18058  slwispgp  18072  sylow2alem1  18078  oppglsm  18103  efgsdmi  18191  efgsrel  18193  efgsp1  18196  efgsres  18197  efgcpbllemb  18214  efgcpbl  18215  srgi  18557  srgrz  18572  srglz  18573  ringi  18606  ringsrg  18635  irredmul  18755  lmodlema  18916  lsscl  18991  phllmhm  20025  ipcj  20027  ipeq0  20031  ocvi  20061  obsip  20113  obsocv  20118  2ndcctbss  21306  locfinnei  21374  fclssscls  21869  tmdcn  21934  tgpinv  21936  trgtmd  22015  tdrgunit  22017  ngpds  22455  nrmtngdist  22508  elii1  22781  elii2  22782  icopnfcnv  22788  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  phtpcer  22841  pcoass  22870  clmsubrg  22912  cphnmfval  23038  bnsca  23182  uc1pldg  23953  mon1pldg  23954  sinq12ge0  24305  cosq14gt0  24307  cosq14ge0  24308  sinord  24325  recosf1o  24326  resinf1o  24327  logrnaddcl  24366  logimul  24405  dvlog2lem  24443  atanf  24652  atanneg  24679  atancj  24682  efiatan  24684  atanlogaddlem  24685  atanlogadd  24686  atanlogsub  24688  efiatan2  24689  2efiatan  24690  ressatans  24706  dvatan  24707  areaf  24733  harmonicubnd  24781  harmonicbnd4  24782  lgamgulmlem2  24801  2sqlem2  25188  2sqlem3  25190  dchrvmasumiflem1  25235  pntpbnd2  25321  f1otrg  25796  f1otrge  25797  brbtwn2  25830  ax5seglem3  25856  axpaschlem  25865  axcontlem7  25895  hstel2  29206  stle1  29212  stj  29222  xrge0adddir  29820  omndadd  29834  slmdlema  29884  lmodslmd  29885  orngmul  29931  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  rrextcusp  30177  rrextust  30180  unelros  30362  difelros  30363  inelsros  30369  diffiunisros  30370  sibfinima  30529  eulerpartlemf  30560  eulerpartlemgvv  30566  bnj563  30939  bnj1366  31026  bnj1379  31027  bnj554  31095  bnj557  31097  bnj570  31101  bnj594  31108  bnj1001  31154  bnj1006  31155  bnj1097  31175  bnj1177  31200  bnj1388  31227  bnj1398  31228  bnj1450  31244  bnj1501  31261  bnj1523  31265  snmlflim  31440  msrval  31561  mclsssvlem  31585  mclsind  31593  ptrecube  33539  cntotbnd  33725  heiborlem8  33747  dmnnzd  34004  atlex  34921  kelac1  37950  binomcxplemcvg  38870  binomcxplemnotnn0  38872  elixpconstg  39580  fvixp2  39703  stoweidlem39  40574  stoweidlem60  40595  fourierdlem40  40682  fourierdlem78  40719  isringrng  42206
  Copyright terms: Public domain W3C validator