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

Theorem syl5bbr 250
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 193 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 248 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1789  19.19  1791  sbco2  2025  cbvab  2402  necon1bbid  2501  necon4abid  2511  elabgt  2912  sbceq1a  3002  sbcralt  3064  sbccsbg  3110  sbccsb2g  3111  disjxun  4022  iunpw  4569  ordunisuc2  4634  tfis  4644  tfinds  4649  dfom2  4657  xp11  5110  ressn  5209  fnssresb  5322  fun11iun  5459  dmfco  5555  dffo4  5638  f1ompt  5644  funressn  5668  fnsuppeq0  5695  elunirn  5739  fliftf  5776  resoprab2  5903  ralrnmpt2  5920  1stconst  6169  2ndconst  6170  opiota  6284  iinon  6353  dfsmo2  6360  oeeui  6596  omabs  6641  brecop  6747  ixpsnf1o  6852  boxcutc  6855  ac6sfi  7097  wemapwe  7396  sdom2en01  7924  ac6num  8102  zorn2lem7  8125  ttukeylem6  8137  alephval2  8190  fpwwe2  8261  fpwwe  8264  nqereu  8549  suplem2pr  8673  map2psrpr  8728  supsrlem  8729  fimaxre3  9699  infm3  9709  crne0  9735  nn1suc  9763  uzindOLD  10102  xmulneg1  10585  supxrbnd1  10636  supxrbnd2  10637  iccneg  10753  wrdind  11473  cnpart  11721  sqr00  11745  lo1resb  12034  o1resb  12036  absefib  12474  efieq1re  12475  sadadd2lem2  12637  saddisjlem  12651  prmind2  12765  mreacs  13556  issubc  13708  isfunc  13734  pospo  14103  eqgval  14662  resscntz  14803  frgpuplem  15077  divsabl  15153  dmdprd  15232  dprdcntz2  15269  dprd2d2  15275  isnzr2  16011  chrdvds  16478  chrcong  16479  znleval  16504  isphld  16554  isclo  16820  ist1-2  17071  isnrm2  17082  nconsubb  17145  subislly  17203  ptclsg  17305  qtopcld  17400  kqcldsat  17420  divstgplem  17799  tsmssubm  17821  caucfil  18705  ioorinv  18927  mbfss  18997  iblss2  19156  dvivthlem1  19351  lhop1  19357  mpfind  19424  pf1ind  19434  deg1leb  19477  reeff1o  19819  sincosq3sgn  19864  sincosq4sgn  19865  dcubic  20138  efrlim  20260  fsumharmonic  20301  isppw  20348  issqf  20370  fsumdvdsmul  20431  ppiub  20439  lgsdinn0  20575  h2hlm  21556  isch2  21799  ch0pss  22020  nmcfnlbi  22628  jplem1  22844  hatomistici  22938  mdsymlem5  22983  cdjreui  23008  dfimafnf  23037  ballotlemsima  23070  subfacp1lem2a  23118  subfacp1lem6  23123  eupath2lem2  23309  ghomf1olem  23408  rtrclreclem.trans  23450  dfres3  23522  axlowdimlem14  23993  onsuct0  24290  elo  24451  prodeq3ii  24719  glmrngo  24893  bwt2  25003  lvsovso2  25038  supnuf  25040  supexr  25042  sdclem2  25863  fdc  25866  fdc1  25867  istotbnd3  25906  sstotbnd  25910  prdstotbnd  25929  rrncmslem  25967  diophin  26263  diophun  26264  diophrex  26266  3rexfrabdioph  26289  6rexfrabdioph  26291  7rexfrabdioph  26292  zindbi  26442  fveqsb  27067  stoweidlem35  27195  ndmaovg  27435  bnj1468  28157  lub0N  28658  glb0N  28662  cdlemefrs29bpre0  29864  dvhb1dimN  30454  dvhopellsm  30586  dibord  30628  dochnel2  30861  mapdvalc  31098  mapdval4N  31101
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 177
  Copyright terms: Public domain W3C validator