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

Theorem syl5bbr 259
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1  |-  ( ps  <->  ph )
syl5bbr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bbr  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3  |-  ( ps  <->  ph )
21bicomi 202 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 257 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3bitr3g  287  biass  359  19.16  1883  19.19  1885  sbco2OLD  2112  sbcom2  2151  sbal2  2173  cbvab  2561  necon1bbid  2665  necon4abid  2675  elabgt  3103  sbceq1a  3197  sbcralt  3267  sbccsbgOLD  3702  sbccsb2  3703  sbccsb2gOLD  3704  disjxun  4290  xp11  5273  ressn  5373  fnssresb  5523  dmfco  5765  dffo4  5859  f1ompt  5865  funressn  5895  fnsuppeq0OLD  5939  elunirnALT  5969  fliftf  6008  resoprab2  6187  elrnmpt2res  6204  ralrnmpt2  6205  iunpw  6390  ordunisuc2  6455  tfis  6465  tfinds  6470  dfom2  6478  fun11iun  6537  opiota  6633  1stconst  6661  2ndconst  6662  fnsuppeq0  6717  iinon  6801  dfsmo2  6808  oeeui  7041  omabs  7086  brecop  7193  ixpsnf1o  7303  boxcutc  7306  ac6sfi  7556  wemapwe  7928  wemapweOLD  7929  sdom2en01  8471  ac6num  8648  zorn2lem7  8671  ttukeylem6  8683  alephval2  8736  fpwwe2  8810  fpwwe  8813  nqereu  9098  suplem2pr  9222  map2psrpr  9277  supsrlem  9278  fimaxre3  10279  infm3  10289  crne0  10315  nn1suc  10343  uzindOLD  10736  xmulneg1  11232  supxrbnd1  11284  supxrbnd2  11285  iccneg  11406  wrdind  12371  cnpart  12729  sqr00  12753  lo1resb  13042  o1resb  13044  absefib  13482  efieq1re  13483  sadadd2lem2  13646  saddisjlem  13660  prmind2  13774  mreacs  14596  issubc  14748  isfunc  14774  pospo  15143  mrcmndind  15494  eqgval  15730  resscntz  15849  frgpuplem  16269  divsabl  16347  dmdprd  16480  dprdcntz2  16536  dprd2d2  16543  isnzr2  17345  mpfind  17622  pf1ind  17789  chrdvds  17959  chrcong  17960  znleval  17987  isphld  18083  smadiadetr  18481  isclo  18691  ist1-2  18951  isnrm2  18962  bwth  19013  bwthOLD  19014  nconsubb  19027  subislly  19085  ptclsg  19188  qtopcld  19286  kqcldsat  19306  divstgplem  19691  tsmssubm  19716  ustuqtop  19821  utop2nei  19825  blval2  20150  caucfil  20794  ioorinv  21056  mbfss  21124  iblss2  21283  dvivthlem1  21480  lhop1  21486  deg1leb  21566  reeff1o  21912  sincosq3sgn  21962  sincosq4sgn  21963  dcubic  22241  efrlim  22363  fsumharmonic  22405  isppw  22452  issqf  22474  fsumdvdsmul  22535  ppiub  22543  lgsdinn0  22679  tglngne  22984  tgelrnln  23036  tghilbert1_1  23043  axlowdimlem14  23201  eupath2lem2  23599  h2hlm  24382  isch2  24626  ch0pss  24848  nmcfnlbi  25456  jplem1  25672  hatomistici  25766  mdsymlem5  25811  cdjreui  25836  reuxfr4d  25874  dfimafnf  25950  funcnvmpt  25987  fpwrelmap  26033  nn0min  26090  isarchi  26199  ordtconlem1  26354  esumfsup  26519  esumpcvgval  26527  measvuni  26628  aean  26660  eulerpartlemgh  26761  ballotlemsima  26898  sgn3da  26924  subfacp1lem2a  27068  subfacp1lem6  27073  ghomf1olem  27313  rtrclreclem.trans  27348  dfres3  27569  eldm3  27572  onsuct0  28287  ptrest  28425  sdclem2  28638  fdc  28641  fdc1  28642  istotbnd3  28670  sstotbnd  28674  prdstotbnd  28693  rrncmslem  28731  diophin  29111  diophun  29112  diophrex  29114  3rexfrabdioph  29135  6rexfrabdioph  29137  7rexfrabdioph  29138  zindbi  29287  fveqsb  29709  stoweidlem35  29830  tz6.12-afv  30079  ndmaovg  30090  gsummoncoe1  30843  mp2pm2mplem4  30919  bnj1468  31839  lub0N  32834  glb0N  32838  cdlemefrs29bpre0  34040  dvhb1dimN  34630  dvhopellsm  34762  dibord  34804  dochnel2  35037  mapdvalc  35274  mapdval4N  35277
  Copyright terms: Public domain W3C validator