MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bbr 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  1872  19.19  1874  sbco2  2121  cbvab  2507  necon1bbid  2606  necon4abid  2616  elabgt  3024  sbceq1a  3116  sbcralt  3178  sbccsbg  3224  sbccsb2g  3225  disjxun  4153  iunpw  4701  ordunisuc2  4766  tfis  4776  tfinds  4781  dfom2  4789  xp11  5246  ressn  5350  fnssresb  5499  fun11iun  5637  dmfco  5738  dffo4  5826  f1ompt  5832  funressn  5860  fnsuppeq0  5894  elunirn  5939  fliftf  5978  resoprab2  6108  ralrnmpt2  6125  1stconst  6376  2ndconst  6377  opiota  6473  iinon  6540  dfsmo2  6547  oeeui  6783  omabs  6828  brecop  6935  ixpsnf1o  7040  boxcutc  7043  ac6sfi  7289  wemapwe  7589  sdom2en01  8117  ac6num  8294  zorn2lem7  8317  ttukeylem6  8329  alephval2  8382  fpwwe2  8453  fpwwe  8456  nqereu  8741  suplem2pr  8865  map2psrpr  8920  supsrlem  8921  fimaxre3  9891  infm3  9901  crne0  9927  nn1suc  9955  uzindOLD  10298  xmulneg1  10782  supxrbnd1  10834  supxrbnd2  10835  iccneg  10952  wrdind  11720  cnpart  11974  sqr00  11998  lo1resb  12287  o1resb  12289  absefib  12728  efieq1re  12729  sadadd2lem2  12891  saddisjlem  12905  prmind2  13019  mreacs  13812  issubc  13964  isfunc  13990  pospo  14359  eqgval  14918  resscntz  15059  frgpuplem  15333  divsabl  15409  dmdprd  15488  dprdcntz2  15525  dprd2d2  15531  isnzr2  16263  chrdvds  16734  chrcong  16735  znleval  16760  isphld  16810  isclo  17076  ist1-2  17335  isnrm2  17346  nconsubb  17409  subislly  17467  ptclsg  17570  qtopcld  17668  kqcldsat  17688  divstgplem  18073  tsmssubm  18095  ustuqtop  18199  utop2nei  18203  blval2  18484  caucfil  19109  ioorinv  19337  mbfss  19407  iblss2  19566  dvivthlem1  19761  lhop1  19767  mpfind  19834  pf1ind  19844  deg1leb  19887  reeff1o  20232  sincosq3sgn  20277  sincosq4sgn  20278  dcubic  20555  efrlim  20677  fsumharmonic  20719  isppw  20766  issqf  20788  fsumdvdsmul  20849  ppiub  20857  lgsdinn0  20993  eupath2lem2  21550  h2hlm  22333  isch2  22576  ch0pss  22797  nmcfnlbi  23405  jplem1  23621  hatomistici  23715  mdsymlem5  23760  cdjreui  23785  reuxfr4d  23823  dfimafnf  23888  funcnvmpt  23926  esumfsup  24258  esumpcvgval  24266  measvuni  24364  aean  24391  ballotlemsima  24554  subfacp1lem2a  24647  subfacp1lem6  24652  ghomf1olem  24886  rtrclreclem.trans  24927  dfres3  25142  eldm3  25145  axlowdimlem14  25610  onsuct0  25907  sdclem2  26139  fdc  26142  fdc1  26143  istotbnd3  26173  sstotbnd  26177  prdstotbnd  26196  rrncmslem  26234  diophin  26524  diophun  26525  diophrex  26527  3rexfrabdioph  26550  6rexfrabdioph  26552  7rexfrabdioph  26553  zindbi  26702  fveqsb  27326  stoweidlem35  27454  tz6.12-afv  27708  ndmaovg  27719  frgra2v  27754  bnj1468  28557  sbco2wAUX7  28922  sbco2OLD7  29070  lub0N  29306  glb0N  29310  cdlemefrs29bpre0  30512  dvhb1dimN  31102  dvhopellsm  31234  dibord  31276  dochnel2  31509  mapdvalc  31746  mapdval4N  31749
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