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

Theorem simp3bi 1022
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 197 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 1019 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  limuni  5498  smores2  7077  ersym  7379  ertr  7382  fvixp  7531  undifixp  7562  fiint  7850  winalim2  9121  inar1  9200  supmullem1  10577  supmullem2  10578  supmul  10579  eluzle  11171  ico01fl0  12052  ef01bndlem  14223  sin01bnd  14224  cos01bnd  14225  sin01gt0  14229  divalglem6  14363  gznegcl  14864  gzcjcl  14865  gzaddcl  14866  gzmulcl  14867  gzabssqcl  14870  4sqlem4a  14880  prdsbasprj  15355  xpsff1o  15459  mreintcl  15486  drsdir  16165  subggrp  16805  pmtrfconj  17092  symggen  17096  psgnunilem1  17119  subgpgp  17234  slwispgp  17248  sylow2alem1  17254  oppglsm  17279  efgsdmi  17367  efgsrel  17369  efgsp1  17372  efgsres  17373  efgcpbllemb  17390  efgcpbl  17391  srgi  17730  srgrz  17744  srglz  17745  ringi  17778  ringsrg  17804  irredmul  17922  lmodlema  18081  lsscl  18151  phllmhm  19183  ipcj  19185  ipeq0  19189  ocvi  19216  obsip  19268  obsocv  19273  2ndcctbss  20454  locfinnei  20522  fclssscls  21017  tmdcn  21082  tgpinv  21084  trgtmd  21163  tdrgunit  21165  ngpds  21601  elii1  21947  elii2  21948  icopnfcnv  21954  icopnfhmeo  21955  iccpnfhmeo  21957  xrhmeo  21958  phtpcer  22010  pcoass  22039  clmsubrg  22081  cphnmfval  22154  bnsca  22291  uc1pldg  23083  mon1pldg  23084  sinq12ge0  23447  cosq14gt0  23449  cosq14ge0  23450  sinord  23467  recosf1o  23468  resinf1o  23469  logrnaddcl  23508  logimul  23547  dvlog2lem  23581  atanf  23790  atanneg  23817  atancj  23820  efiatan  23822  atanlogaddlem  23823  atanlogadd  23824  atanlogsub  23826  efiatan2  23827  2efiatan  23828  ressatans  23844  dvatan  23845  areaf  23871  harmonicubnd  23919  harmonicbnd4  23920  lgamgulmlem2  23939  2sqlem2  24276  2sqlem3  24278  dchrvmasumiflem1  24323  pntpbnd2  24409  f1otrg  24885  f1otrge  24886  brbtwn2  24919  ax5seglem3  24945  axpaschlem  24954  axcontlem7  24984  subgores  26015  hstel2  27855  stle1  27861  stj  27871  xrge0adddir  28447  omndadd  28461  slmdlema  28511  lmodslmd  28512  orngmul  28559  xrge0iifcnv  28732  xrge0iifiso  28734  xrge0iifhom  28736  rrextcusp  28802  rrextust  28805  unelros  28986  difelros  28987  inelsros  28993  diffiunisros  28994  sibfinima  29165  eulerpartlemf  29196  eulerpartlemgvv  29202  bnj563  29546  bnj1366  29634  bnj1379  29635  bnj554  29703  bnj557  29705  bnj570  29709  bnj594  29716  bnj1001  29762  bnj1006  29763  bnj1097  29783  bnj1177  29808  bnj1388  29835  bnj1398  29836  bnj1450  29852  bnj1501  29869  bnj1523  29873  snmlflim  30048  msrval  30169  mclsssvlem  30193  mclsind  30201  ptrecube  31851  cntotbnd  32039  heiborlem8  32061  dmnnzd  32219  atlex  32798  kelac1  35838  binomcxplemcvg  36558  binomcxplemnotnn0  36560  stoweidlem39  37717  stoweidlem60  37738  fourierdlem40  37827  fourierdlem78  37865  isringrng  39067
  Copyright terms: Public domain W3C validator