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

Theorem syl5bbr 252
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 195 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 250 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  3bitr3g  280  biass  350  19.16  1767  19.19  1769  sbco2  1981  cbvab  2376  necon1bbid  2475  necon4abid  2485  elabgt  2886  sbceq1a  2976  sbcralt  3038  sbccsbg  3084  sbccsb2g  3085  disjxun  3995  iunpw  4542  ordunisuc2  4607  tfis  4617  tfinds  4622  dfom2  4630  xp11  5099  ressn  5198  fnssresb  5294  fun11iun  5431  dmfco  5527  dffo4  5610  f1ompt  5616  funressn  5640  fnsuppeq0  5667  elunirn  5711  fliftf  5748  resoprab2  5875  ralrnmpt2  5892  1stconst  6141  2ndconst  6142  opiota  6256  iinon  6325  dfsmo2  6332  oeeui  6568  omabs  6613  brecop  6719  ixpsnf1o  6824  boxcutc  6827  ac6sfi  7069  wemapwe  7368  sdom2en01  7896  ac6num  8074  zorn2lem7  8097  ttukeylem6  8109  alephval2  8162  fpwwe2  8233  fpwwe  8236  nqereu  8521  suplem2pr  8645  map2psrpr  8700  supsrlem  8701  fimaxre3  9671  infm3  9681  crne0  9707  nn1suc  9735  uzindOLD  10074  xmulneg1  10556  supxrbnd1  10607  supxrbnd2  10608  iccneg  10724  wrdind  11443  cnpart  11691  sqr00  11715  lo1resb  12004  o1resb  12006  absefib  12441  efieq1re  12442  sadadd2lem2  12604  saddisjlem  12618  prmind2  12732  mreacs  13523  issubc  13675  isfunc  13701  pospo  14070  eqgval  14629  resscntz  14770  frgpuplem  15044  divsabl  15120  dmdprd  15199  dprdcntz2  15236  dprd2d2  15242  isnzr2  15978  chrdvds  16445  chrcong  16446  znleval  16471  isphld  16521  isclo  16787  ist1-2  17038  isnrm2  17049  nconsubb  17112  subislly  17170  ptclsg  17272  qtopcld  17367  kqcldsat  17387  divstgplem  17766  tsmssubm  17788  caucfil  18672  ioorinv  18894  mbfss  18964  iblss2  19123  dvivthlem1  19318  lhop1  19324  mpfind  19391  pf1ind  19401  deg1leb  19444  reeff1o  19786  sincosq3sgn  19831  sincosq4sgn  19832  dcubic  20105  efrlim  20227  fsumharmonic  20268  isppw  20315  issqf  20337  fsumdvdsmul  20398  ppiub  20406  lgsdinn0  20542  h2hlm  21521  isch2  21764  ch0pss  21985  nmcfnlbi  22593  jplem1  22809  hatomistici  22903  mdsymlem5  22948  cdjreui  22973  dfimafnf  23003  ballotlemsima  23036  subfacp1lem2a  23084  subfacp1lem6  23089  eupath2lem2  23275  ghomf1olem  23374  rtrclreclem.trans  23416  dfres3  23488  axlowdimlem14  23959  onsuct0  24256  elo  24408  prodeq3ii  24676  glmrngo  24850  bwt2  24960  lvsovso2  24995  supnuf  24997  supexr  24999  sdclem2  25820  fdc  25823  fdc1  25824  istotbnd3  25863  sstotbnd  25867  prdstotbnd  25886  rrncmslem  25924  diophin  26220  diophun  26221  diophrex  26223  3rexfrabdioph  26246  6rexfrabdioph  26248  7rexfrabdioph  26249  zindbi  26399  fveqsb  27025  stoweidlem35  27153  bnj1468  28010  lub0N  28629  glb0N  28633  cdlemefrs29bpre0  29835  dvhb1dimN  30425  dvhopellsm  30557  dibord  30599  dochnel2  30832  mapdvalc  31069  mapdval4N  31072
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator