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  2120  cbvab  2506  necon1bbid  2605  necon4abid  2615  elabgt  3023  sbceq1a  3115  sbcralt  3177  sbccsbg  3223  sbccsb2g  3224  disjxun  4152  iunpw  4700  ordunisuc2  4765  tfis  4775  tfinds  4780  dfom2  4788  xp11  5245  ressn  5349  fnssresb  5498  fun11iun  5636  dmfco  5737  dffo4  5825  f1ompt  5831  funressn  5859  fnsuppeq0  5893  elunirn  5938  fliftf  5977  resoprab2  6107  ralrnmpt2  6124  1stconst  6375  2ndconst  6376  opiota  6472  iinon  6539  dfsmo2  6546  oeeui  6782  omabs  6827  brecop  6934  ixpsnf1o  7039  boxcutc  7042  ac6sfi  7288  wemapwe  7588  sdom2en01  8116  ac6num  8293  zorn2lem7  8316  ttukeylem6  8328  alephval2  8381  fpwwe2  8452  fpwwe  8455  nqereu  8740  suplem2pr  8864  map2psrpr  8919  supsrlem  8920  fimaxre3  9890  infm3  9900  crne0  9926  nn1suc  9954  uzindOLD  10297  xmulneg1  10781  supxrbnd1  10833  supxrbnd2  10834  iccneg  10951  wrdind  11719  cnpart  11973  sqr00  11997  lo1resb  12286  o1resb  12288  absefib  12727  efieq1re  12728  sadadd2lem2  12890  saddisjlem  12904  prmind2  13018  mreacs  13811  issubc  13963  isfunc  13989  pospo  14358  eqgval  14917  resscntz  15058  frgpuplem  15332  divsabl  15408  dmdprd  15487  dprdcntz2  15524  dprd2d2  15530  isnzr2  16262  chrdvds  16733  chrcong  16734  znleval  16759  isphld  16809  isclo  17075  ist1-2  17334  isnrm2  17345  nconsubb  17408  subislly  17466  ptclsg  17569  qtopcld  17667  kqcldsat  17687  divstgplem  18072  tsmssubm  18094  ustuqtop  18198  utop2nei  18202  blval2  18483  caucfil  19108  ioorinv  19336  mbfss  19406  iblss2  19565  dvivthlem1  19760  lhop1  19766  mpfind  19833  pf1ind  19843  deg1leb  19886  reeff1o  20231  sincosq3sgn  20276  sincosq4sgn  20277  dcubic  20554  efrlim  20676  fsumharmonic  20718  isppw  20765  issqf  20787  fsumdvdsmul  20848  ppiub  20856  lgsdinn0  20992  eupath2lem2  21549  h2hlm  22332  isch2  22575  ch0pss  22796  nmcfnlbi  23404  jplem1  23620  hatomistici  23714  mdsymlem5  23759  cdjreui  23784  reuxfr4d  23822  dfimafnf  23887  funcnvmpt  23925  esumfsup  24257  esumpcvgval  24265  measvuni  24363  aean  24390  ballotlemsima  24553  subfacp1lem2a  24646  subfacp1lem6  24651  ghomf1olem  24885  rtrclreclem.trans  24926  dfres3  25141  eldm3  25144  axlowdimlem14  25609  onsuct0  25906  sdclem2  26138  fdc  26141  fdc1  26142  istotbnd3  26172  sstotbnd  26176  prdstotbnd  26195  rrncmslem  26233  diophin  26523  diophun  26524  diophrex  26526  3rexfrabdioph  26549  6rexfrabdioph  26551  7rexfrabdioph  26552  zindbi  26701  fveqsb  27325  stoweidlem35  27453  tz6.12-afv  27707  ndmaovg  27718  frgra2v  27753  bnj1468  28556  sbco2wAUX7  28921  sbco2OLD7  29069  lub0N  29305  glb0N  29309  cdlemefrs29bpre0  30511  dvhb1dimN  31101  dvhopellsm  31233  dibord  31275  dochnel2  31508  mapdvalc  31745  mapdval4N  31748
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