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

Theorem simp3bi 1076
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 1073 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  limuni  5744  smores2  7396  ersym  7699  ertr  7702  fvixp  7857  undifixp  7888  fiint  8181  winalim2  9462  inar1  9541  supmullem1  10937  supmullem2  10938  supmul  10939  eluzle  11644  ico01fl0  12560  ef01bndlem  14839  sin01bnd  14840  cos01bnd  14841  sin01gt0  14845  divalglem6  15045  gznegcl  15563  gzcjcl  15564  gzaddcl  15565  gzmulcl  15566  gzabssqcl  15569  4sqlem4a  15579  prdsbasprj  16053  xpsff1o  16149  mreintcl  16176  drsdir  16856  subggrp  17518  pmtrfconj  17807  symggen  17811  psgnunilem1  17834  subgpgp  17933  slwispgp  17947  sylow2alem1  17953  oppglsm  17978  efgsdmi  18066  efgsrel  18068  efgsp1  18071  efgsres  18072  efgcpbllemb  18089  efgcpbl  18090  srgi  18432  srgrz  18447  srglz  18448  ringi  18481  ringsrg  18510  irredmul  18630  lmodlema  18789  lsscl  18862  phllmhm  19896  ipcj  19898  ipeq0  19902  ocvi  19932  obsip  19984  obsocv  19989  2ndcctbss  21168  locfinnei  21236  fclssscls  21732  tmdcn  21797  tgpinv  21799  trgtmd  21878  tdrgunit  21880  ngpds  22318  nrmtngdist  22371  elii1  22642  elii2  22643  icopnfcnv  22649  icopnfhmeo  22650  iccpnfhmeo  22652  xrhmeo  22653  phtpcer  22702  phtpcerOLD  22703  pcoass  22732  clmsubrg  22774  cphnmfval  22900  bnsca  23044  uc1pldg  23812  mon1pldg  23813  sinq12ge0  24164  cosq14gt0  24166  cosq14ge0  24167  sinord  24184  recosf1o  24185  resinf1o  24186  logrnaddcl  24225  logimul  24264  dvlog2lem  24298  atanf  24507  atanneg  24534  atancj  24537  efiatan  24539  atanlogaddlem  24540  atanlogadd  24541  atanlogsub  24543  efiatan2  24544  2efiatan  24545  ressatans  24561  dvatan  24562  areaf  24588  harmonicubnd  24636  harmonicbnd4  24637  lgamgulmlem2  24656  2sqlem2  25043  2sqlem3  25045  dchrvmasumiflem1  25090  pntpbnd2  25176  f1otrg  25651  f1otrge  25652  brbtwn2  25685  ax5seglem3  25711  axpaschlem  25720  axcontlem7  25750  hstel2  28927  stle1  28933  stj  28943  xrge0adddir  29477  omndadd  29491  slmdlema  29541  lmodslmd  29542  orngmul  29588  xrge0iifcnv  29761  xrge0iifiso  29763  xrge0iifhom  29765  rrextcusp  29831  rrextust  29834  unelros  30015  difelros  30016  inelsros  30022  diffiunisros  30023  sibfinima  30182  eulerpartlemf  30213  eulerpartlemgvv  30219  bnj563  30521  bnj1366  30608  bnj1379  30609  bnj554  30677  bnj557  30679  bnj570  30683  bnj594  30690  bnj1001  30736  bnj1006  30737  bnj1097  30757  bnj1177  30782  bnj1388  30809  bnj1398  30810  bnj1450  30826  bnj1501  30843  bnj1523  30847  snmlflim  31022  msrval  31143  mclsssvlem  31167  mclsind  31175  ptrecube  33041  cntotbnd  33227  heiborlem8  33249  dmnnzd  33506  atlex  34083  kelac1  37113  binomcxplemcvg  38035  binomcxplemnotnn0  38037  elixpconstg  38751  fvixp2  38863  stoweidlem39  39563  stoweidlem60  39584  fourierdlem40  39671  fourierdlem78  39708  isringrng  41169
  Copyright terms: Public domain W3C validator