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  2374  necon1bbid  2473  necon4abid  2483  elabgt  2862  sbceq1a  2945  sbcralt  3007  sbccsbg  3051  sbccsb2g  3052  disjxun  3961  iunpw  4507  ordunisuc2  4572  tfis  4582  tfinds  4587  dfom2  4595  xp11  5064  ressn  5163  fnssresb  5259  fun11iun  5396  dmfco  5492  dffo4  5575  f1ompt  5581  funressn  5605  fnsuppeq0  5632  elunirn  5676  fliftf  5713  resoprab2  5840  ralrnmpt2  5857  1stconst  6106  2ndconst  6107  opiota  6221  iinon  6290  dfsmo2  6297  oeeui  6533  omabs  6578  brecop  6684  ixpsnf1o  6789  boxcutc  6792  ac6sfi  7034  wemapwe  7333  sdom2en01  7861  ac6num  8039  zorn2lem7  8062  ttukeylem6  8074  alephval2  8127  fpwwe2  8198  fpwwe  8201  nqereu  8486  suplem2pr  8610  map2psrpr  8665  supsrlem  8666  fimaxre3  9636  infm3  9646  crne0  9672  nn1suc  9700  uzindOLD  10038  xmulneg1  10520  supxrbnd1  10571  supxrbnd2  10572  iccneg  10688  wrdind  11407  cnpart  11655  sqr00  11679  lo1resb  11968  o1resb  11970  absefib  12405  efieq1re  12406  sadadd2lem2  12568  saddisjlem  12582  prmind2  12696  mreacs  13487  issubc  13639  isfunc  13665  pospo  14034  eqgval  14593  resscntz  14734  frgpuplem  15008  0frgp  15015  divsabl  15084  dmdprd  15163  dprdcntz2  15200  dprd2d2  15206  isnzr2  15942  chrdvds  16409  chrcong  16410  znleval  16435  isphld  16485  isclo  16751  ist1-2  17002  isnrm2  17013  nconsubb  17076  subislly  17134  ptclsg  17236  qtopcld  17331  kqcldsat  17351  divstgplem  17730  tsmssubm  17752  caucfil  18636  ioorinv  18858  mbfss  18928  iblss2  19087  dvivthlem1  19282  lhop1  19288  mpfind  19355  pf1ind  19365  deg1leb  19408  reeff1o  19750  sincosq3sgn  19795  sincosq4sgn  19796  dcubic  20069  efrlim  20191  fsumharmonic  20232  isppw  20279  issqf  20301  fsumdvdsmul  20362  ppiub  20370  lgsdinn0  20506  h2hlm  21485  isch2  21728  ch0pss  21949  nmcfnlbi  22557  jplem1  22773  hatomistici  22867  mdsymlem5  22912  cdjreui  22937  dfimafnf  22967  ballotlemsima  23000  subfacp1lem2a  23048  subfacp1lem6  23053  eupath2lem2  23239  ghomf1olem  23338  rtrclreclem.trans  23380  dfres3  23452  axlowdimlem14  23923  onsuct0  24220  elo  24372  prodeq3ii  24640  glmrngo  24814  bwt2  24924  lvsovso2  24959  supnuf  24961  supexr  24963  sdclem2  25784  fdc  25787  fdc1  25788  istotbnd3  25827  sstotbnd  25831  prdstotbnd  25850  rrncmslem  25888  diophin  26184  diophun  26185  diophrex  26187  3rexfrabdioph  26210  6rexfrabdioph  26212  7rexfrabdioph  26213  zindbi  26363  fveqsb  26989  stoweidlem35  27084  bnj1468  27890  lub0N  28509  glb0N  28513  cdlemefrs29bpre0  29715  dvhb1dimN  30305  dvhopellsm  30437  dibord  30479  dochnel2  30712  mapdvalc  30949  mapdval4N  30952
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