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

Theorem syl5bbr 251
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 194 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 249 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitr3g  279  biass  349  19.16  1883  19.19  1885  sbco2  2161  cbvab  2553  necon1bbid  2652  necon4abid  2662  elabgt  3071  sbceq1a  3163  sbcralt  3225  sbccsbg  3271  sbccsb2g  3272  disjxun  4202  iunpw  4751  ordunisuc2  4816  tfis  4826  tfinds  4831  dfom2  4839  xp11  5296  ressn  5400  fnssresb  5549  fun11iun  5687  dmfco  5789  dffo4  5877  f1ompt  5883  funressn  5911  fnsuppeq0  5945  elunirn  5990  fliftf  6029  resoprab2  6159  ralrnmpt2  6176  1stconst  6427  2ndconst  6428  opiota  6527  iinon  6594  dfsmo2  6601  oeeui  6837  omabs  6882  brecop  6989  ixpsnf1o  7094  boxcutc  7097  ac6sfi  7343  wemapwe  7646  sdom2en01  8174  ac6num  8351  zorn2lem7  8374  ttukeylem6  8386  alephval2  8439  fpwwe2  8510  fpwwe  8513  nqereu  8798  suplem2pr  8922  map2psrpr  8977  supsrlem  8978  fimaxre3  9949  infm3  9959  crne0  9985  nn1suc  10013  uzindOLD  10356  xmulneg1  10840  supxrbnd1  10892  supxrbnd2  10893  iccneg  11010  wrdind  11783  cnpart  12037  sqr00  12061  lo1resb  12350  o1resb  12352  absefib  12791  efieq1re  12792  sadadd2lem2  12954  saddisjlem  12968  prmind2  13082  mreacs  13875  issubc  14027  isfunc  14053  pospo  14422  eqgval  14981  resscntz  15122  frgpuplem  15396  divsabl  15472  dmdprd  15551  dprdcntz2  15588  dprd2d2  15594  isnzr2  16326  chrdvds  16801  chrcong  16802  znleval  16827  isphld  16877  isclo  17143  ist1-2  17403  isnrm2  17414  bwth  17465  nconsubb  17478  subislly  17536  ptclsg  17639  qtopcld  17737  kqcldsat  17757  divstgplem  18142  tsmssubm  18164  ustuqtop  18268  utop2nei  18272  blval2  18597  caucfil  19228  ioorinv  19460  mbfss  19530  iblss2  19689  dvivthlem1  19884  lhop1  19890  mpfind  19957  pf1ind  19967  deg1leb  20010  reeff1o  20355  sincosq3sgn  20400  sincosq4sgn  20401  dcubic  20678  efrlim  20800  fsumharmonic  20842  isppw  20889  issqf  20911  fsumdvdsmul  20972  ppiub  20980  lgsdinn0  21116  eupath2lem2  21692  h2hlm  22475  isch2  22718  ch0pss  22939  nmcfnlbi  23547  jplem1  23763  hatomistici  23857  mdsymlem5  23902  cdjreui  23927  reuxfr4d  23969  dfimafnf  24035  funcnvmpt  24075  isarchi  24244  esumfsup  24452  esumpcvgval  24460  measvuni  24560  aean  24587  ballotlemsima  24765  subfacp1lem2a  24858  subfacp1lem6  24863  ghomf1olem  25097  rtrclreclem.trans  25138  dfres3  25374  eldm3  25377  axlowdimlem14  25886  onsuct0  26183  sdclem2  26437  fdc  26440  fdc1  26441  istotbnd3  26471  sstotbnd  26475  prdstotbnd  26494  rrncmslem  26532  diophin  26822  diophun  26823  diophrex  26825  3rexfrabdioph  26848  6rexfrabdioph  26850  7rexfrabdioph  26851  zindbi  27000  fveqsb  27623  stoweidlem35  27751  tz6.12-afv  28004  ndmaovg  28015  frgra2v  28326  bnj1468  29154  sbco2wAUX7  29522  ax7w15lemAUX7  29604  sbco2OLD7  29689  lub0N  29924  glb0N  29928  cdlemefrs29bpre0  31130  dvhb1dimN  31720  dvhopellsm  31852  dibord  31894  dochnel2  32127  mapdvalc  32364  mapdval4N  32367
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 178
  Copyright terms: Public domain W3C validator