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

Theorem simp3bi 972
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
simp3bi  |-  ( ph  ->  th )

Proof of Theorem simp3bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 969 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  limuni  4489  smores2  6413  ersym  6714  ertr  6717  fvixp  6864  undifixp  6895  fiint  7178  winalim2  8363  inar1  8442  supmullem1  9765  supmullem2  9766  supmul  9767  eluzle  10287  ef01bndlem  12511  sin01bnd  12512  cos01bnd  12513  sin01gt0  12517  divalglem6  12644  gznegcl  13029  gzcjcl  13030  gzaddcl  13031  gzmulcl  13032  gzabssqcl  13035  4sqlem4a  13045  prdsbasprj  13420  xpsff1o  13519  mreintcl  13546  drsdir  14118  subggrp  14673  subgpgp  14957  slwispgp  14971  sylow2alem1  14977  oppglsm  15002  efgsdmi  15090  efgsrel  15092  efgsp1  15095  efgsres  15096  efgcpbllemb  15113  efgcpbl  15114  rngi  15402  irredmul  15540  lmodlema  15681  lsscl  15749  phllmhm  16592  ipcj  16594  ipeq0  16598  ocvi  16625  obsip  16677  obsocv  16682  2ndcctbss  17237  fclssscls  17765  tmdcn  17818  tgpinv  17820  trgtmd  17899  tdrgunit  17901  ngpds  18177  elii1  18486  elii2  18487  icopnfcnv  18493  icopnfhmeo  18494  iccpnfhmeo  18496  xrhmeo  18497  phtpcer  18546  pcoass  18575  clmsubrg  18617  cphnmfval  18681  bnsca  18814  uc1pldg  19587  mon1pldg  19588  sinq12ge0  19929  cosq14gt0  19931  cosq14ge0  19932  sinord  19949  recosf1o  19950  resinf1o  19951  logrnaddcl  19984  logimul  20021  dvlog2lem  20052  atanf  20229  atanneg  20256  atancj  20259  efiatan  20261  atanlogaddlem  20262  atanlogadd  20263  atanlogsub  20265  efiatan2  20266  2efiatan  20267  ressatans  20283  dvatan  20284  areaf  20309  harmonicubnd  20356  harmonicbnd4  20357  2sqlem2  20656  2sqlem3  20658  dchrvmasumiflem1  20703  pntpbnd2  20789  subgores  21024  hstel2  22854  stle1  22860  stj  22870  xrge0adddir  23353  iistmd  23369  xrge0iifcnv  23388  xrge0iifiso  23390  snmlflim  24199  brbtwn2  24919  ax5seglem3  24945  axpaschlem  24954  axcontlem7  24984  locfinnei  25451  cntotbnd  25668  heiborlem8  25690  dmnnzd  25848  kelac1  26309  pmtrfconj  26555  symggen  26559  psgnunilem1  26564  stoweidlem39  26936  stoweidlem60  26957  bnj563  28283  bnj1366  28373  bnj1379  28374  bnj554  28442  bnj557  28444  bnj570  28448  bnj594  28455  bnj1001  28501  bnj1006  28502  bnj1097  28522  bnj1177  28547  bnj1388  28574  bnj1398  28575  bnj1450  28591  bnj1501  28608  bnj1523  28612  atlex  29324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator