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

Theorem simp3bi 1170
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 207 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp3d 1167 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:  limuni  5998  smores2  7687  ersym  7991  ertr  7994  fvixp  8150  undifixp  8181  fiint  8476  winalim2  9803  inar1  9882  supmullem1  11278  supmullem2  11279  supmul  11280  eluzle  11917  ico01fl0  12844  ef01bndlem  15134  sin01bnd  15135  cos01bnd  15136  sin01gt0  15140  divalglem6  15341  gznegcl  15856  gzcjcl  15857  gzaddcl  15858  gzmulcl  15859  gzabssqcl  15862  4sqlem4a  15872  prdsbasprj  16337  xpsff1o  16433  mreintcl  16460  drsdir  17140  subggrp  17799  pmtrfconj  18087  symggen  18091  psgnunilem1  18114  subgpgp  18213  slwispgp  18227  sylow2alem1  18233  oppglsm  18258  efgsdmi  18346  efgsrel  18348  efgsp1  18351  efgsres  18352  efgcpbllemb  18369  efgcpbl  18370  srgi  18713  srgrz  18728  srglz  18729  ringi  18762  ringsrg  18791  irredmul  18911  lmodlema  19072  lsscl  19147  phllmhm  20187  ipcj  20189  ipeq0  20193  ocvi  20223  obsip  20275  obsocv  20280  2ndcctbss  21472  locfinnei  21540  fclssscls  22035  tmdcn  22100  tgpinv  22102  trgtmd  22181  tdrgunit  22183  ngpds  22621  nrmtngdist  22674  elii1  22947  elii2  22948  icopnfcnv  22954  icopnfhmeo  22955  iccpnfhmeo  22957  xrhmeo  22958  phtpcer  23007  pcoass  23036  clmsubrg  23078  cphnmfval  23204  bnsca  23348  uc1pldg  24122  mon1pldg  24123  sinq12ge0  24475  cosq14gt0  24477  cosq14ge0  24478  sinord  24495  recosf1o  24496  resinf1o  24497  logrnaddcl  24535  logimul  24574  dvlog2lem  24612  atanf  24821  atanneg  24848  atancj  24851  efiatan  24853  atanlogaddlem  24854  atanlogadd  24855  atanlogsub  24857  efiatan2  24858  2efiatan  24859  ressatans  24875  dvatan  24876  areaf  24902  harmonicubnd  24950  harmonicbnd4  24951  lgamgulmlem2  24970  2sqlem2  25357  2sqlem3  25359  dchrvmasumiflem1  25404  pntpbnd2  25490  f1otrg  25965  f1otrge  25966  brbtwn2  25999  ax5seglem3  26025  axpaschlem  26034  axcontlem7  26064  hstel2  29406  stle1  29412  stj  29422  xrge0adddir  30017  omndadd  30031  slmdlema  30081  lmodslmd  30082  orngmul  30128  xrge0iifcnv  30304  xrge0iifiso  30306  xrge0iifhom  30308  rrextcusp  30374  rrextust  30377  unelros  30559  difelros  30560  inelsros  30566  diffiunisros  30567  sibfinima  30726  eulerpartlemf  30757  eulerpartlemgvv  30763  bnj563  31136  bnj1366  31223  bnj1379  31224  bnj554  31292  bnj557  31294  bnj570  31298  bnj594  31305  bnj1001  31351  bnj1006  31352  bnj1097  31372  bnj1177  31397  bnj1388  31424  bnj1398  31425  bnj1450  31441  bnj1501  31458  bnj1523  31462  snmlflim  31637  msrval  31758  mclsssvlem  31782  mclsind  31790  ptrecube  33722  cntotbnd  33906  heiborlem8  33928  dmnnzd  34185  atlex  35096  kelac1  38134  binomcxplemcvg  39053  binomcxplemnotnn0  39055  elixpconstg  39759  fvixp2  39877  stoweidlem39  40735  stoweidlem60  40756  fourierdlem40  40843  fourierdlem78  40880  isringrng  42449
  Copyright terms: Public domain W3C validator