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

Theorem syl6bbr 256
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6bbr  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6bbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 195 . 2  |-  ( ch  <->  th )
41, 3syl6bb 254 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3bitr4g  281  bibi2i  306  mtt  331  nbn2  336  3bior1fd  1290  3biant1d  1293  equsalhwOLD  1862  equsalOLD  2001  necon2abid  2663  eueq3  3111  sbcel12g  3268  sbceqg  3269  sbcnel12g  3270  sbcne12g  3271  n0moeu  3642  reldisj  3673  r19.3rz  3721  r19.3rzv  3723  r19.9rzv  3724  ordelpss  4612  reusv2lem5  4731  ordsucun  4808  dflim3  4830  dfom2  4850  peano5  4871  rabxp  4917  elrng  5065  iss  5192  elimasni  5234  eliniseg  5236  xpcan  5308  xpcan2  5309  fcnvres  5623  dffv3  5727  funimass4  5780  fndmdif  5837  fneqeql  5841  funimass3  5849  elrnrexdmb  5878  dff4  5886  fconst4  5959  elunirnALT  6003  eqfnov  6179  caoftrn  6342  mpt2xopovel  6474  brtpos  6491  rntpos  6495  opiota  6538  f1ocnvfv3  6588  ordgt0ge1  6744  ondif2  6749  oelim2  6841  omabs  6893  iiner  6979  erinxp  6981  qliftfun  6992  ordunifi  7360  elfi2  7422  elfiun  7438  fifo  7440  noinfep  7617  cantnfrescl  7635  cantnf  7652  rankonidlem  7757  r1pwOLD  7775  pr2nelem  7893  cardalephex  7976  alephinit  7981  dfac5lem4  8012  cflim2  8148  cfsmolem  8155  compssiso  8259  fin1a2lem11  8295  itunisuc  8304  axdclem  8404  brdom6disj  8415  alephreg  8462  fpwwe2lem9  8518  pwfseqlem3  8540  pwfseqlem4  8542  indpi  8789  nqereu  8811  ordpinq  8825  ltanq  8853  ltmnq  8854  suplem2pr  8935  map2psrpr  8990  ssxr  9150  letri3  9165  leltne  9169  ltneg  9533  leneg  9536  suprnub  9976  negiso  9989  infmrgelb  9993  elnnnn0  10268  nn0sub  10275  zrevaddcl  10326  znnsub  10327  znn0sub  10328  prime  10355  eluz2  10499  indstr  10550  eluz2b1  10552  qrevaddcl  10601  rpneg  10646  xrleltne  10743  dfle2  10745  dflt2  10746  xrletri3  10750  supxrleub  10910  infmxrgelb  10918  ixxin  10938  iccid  10966  elicopnf  11005  iccsplit  11034  fzsplit2  11081  fzsn  11099  fzpr  11106  uzsplit  11123  injresinj  11205  om2uzf1oi  11298  lt2sqi  11475  le2sqi  11476  hashsdom  11660  hashf1lem1  11709  fz1isolem  11715  ccatlcan  11783  ccatrcan  11784  cnpart  12050  limsuplt  12278  rlimresb  12364  mertenslem2  12667  sadadd2lem2  12967  saddisjlem  12981  bitsuz  12991  gcddiv  13054  algcvgblem  13073  isprm2lem  13091  isprm3  13093  isprm5  13117  prmreclem5  13293  vdwapun  13347  vdwmc2  13352  ramcl  13402  pwsle  13719  ismre  13820  mreacs  13888  acsfn  13889  iscatd2  13911  cidpropd  13941  oppcsect2  14005  isfunc  14066  setcinv  14250  tosso  14470  ipodrsfi  14594  acsfiindd  14608  imasmnd2  14737  submacs  14770  imasgrp2  14938  issubg  14949  subgacs  14980  eqgval  14994  gaorber  15090  isslw  15247  sylow2alem2  15257  sylow2a  15258  sylow3lem6  15271  efgcpbllemb  15392  prmcyg  15508  gsum2d2lem  15552  gsumcom2  15554  subgdmdprd  15597  dprd2d2  15607  pgpfac1lem2  15638  pgpfac1lem4  15641  imasrng  15730  drngmulne0  15862  lssle0  16031  lssacs  16048  lssats2  16081  lvecvsn0  16186  islpir  16325  isnzr2  16339  zndvds  16835  znleval  16840  znleval2  16841  eltg2b  17029  discld  17158  opnssneib  17184  cldlp  17219  restbas  17227  leordtvallem1  17279  leordtvallem2  17280  ssidcn  17324  cnprest2  17359  lmss  17367  perfcls  17434  cmpfi  17476  1stccnp  17530  subislly  17549  hausmapdom  17568  iskgen3  17586  kgencn  17593  ptpjpre1  17608  xkoccn  17656  txrest  17668  txlm  17685  txkgen  17689  xkopt  17692  xkoinjcn  17724  imasnopn  17727  imasncld  17728  imasncls  17729  qtopcn  17751  kqfeq  17761  isr0  17774  fbfinnfr  17878  trfbas  17881  fbunfip  17906  ufileu  17956  cfinufil  17965  fmid  17997  txflf  18043  fclsrest  18061  alexsubALT  18087  tsmsres  18178  ucnima  18316  fmucndlem  18326  bldisj  18433  xmeter  18468  elbl4  18611  metuel2  18614  restmetu  18622  dscopn  18626  bl2ioo  18828  isphtpc  19024  tchcph  19199  lmmbr2  19217  lmmbrf  19220  iscau2  19235  iscauf  19238  caucfil  19241  metcld  19263  metcld2  19264  bcthlem1  19282  bcthlem4  19285  cldcss2  19348  ovolgelb  19381  ovoliunlem1  19403  ismbfcn  19526  mbfmax  19544  mbfimaopnlem  19550  i1faddlem  19588  i1fmullem  19589  i1fres  19600  i1fpos  19601  itg1climres  19609  xrge0f  19626  itgresr  19673  iblcnlem1  19682  limcun  19787  dvres  19803  mdegmullem  20006  ply1remlem  20090  plyremlem  20226  vieta1  20234  ulmcau  20316  sineq0  20434  coseq1  20435  ang180lem3  20658  cubic  20694  atandm  20721  atandm2  20722  atandm3  20723  rlimcnp  20809  rlimcnp2  20810  vmappw  20904  dchrelbas3  21027  dchrelbas4  21032  dchrsum2  21057  bposlem6  21078  dchrisumlem3  21190  pntleml  21310  nbgrael  21443  nb3gra2nb  21469  nbcusgra  21477  trls  21541  istrl2  21543  is2wlk  21570  0pth  21575  0spth  21576  wlkdvspthlem  21612  0crct  21618  0cycl  21619  eupath2lem2  21705  elghom  21956  nmoolb  22277  nmlno0lem  22299  ubthlem1  22377  ocsh  22790  shle0  22949  eigrei  23342  adjeu  23397  nmoplb  23415  nmfnlb  23432  eleigvec2  23466  nmlnop0iALT  23503  cnlnadjlem5  23579  adjbdln  23591  jplem2  23777  cvbr2  23791  mdsl2bi  23831  chrelat3  23879  ofpreima  24086  funcnvmpt  24088  funcnv5mpt  24089  gtiso  24093  xrdifh  24148  fzsplit3  24155  toslub  24196  tosglb  24197  xrge0tsmsbi  24229  isarchi  24257  unitdivcld  24304  lmxrge0  24342  eldifpr  24397  eldiftp  24398  issibf  24653  dstfrvunirn  24737  ballotlemfc0  24755  ballotlemfcc  24756  subfacp1lem3  24873  subfacp1lem5  24875  erdszelem9  24890  kur14  24907  iscvm  24951  dfpo2  25383  fundmpss  25395  opelco3  25408  dfon2  25424  elpredg  25458  preduz  25480  nofulllem1  25662  nofulllem2  25663  dfbigcup2  25749  sscoid  25763  funpartfv  25795  dfrdg4  25800  brbtwn2  25849  axsegconlem6  25866  axsegcon  25871  ax5seg  25882  axpasch  25885  axeuclid  25907  axcontlem4  25911  cgr3permute3  25986  segletr  26053  segleantisym  26054  seglelin  26055  cos2h  26251  tan2h  26252  heicant  26253  mbfposadd  26266  cnambfre  26267  dvtanlem  26268  itg2addnclem  26270  itg2addnc  26273  iblabsnclem  26282  ftc1anclem1  26294  ftc1anclem5  26298  fneval  26381  locfindis  26399  neibastop3  26405  eltail  26417  filnetlem4  26424  caures  26480  heiborlem3  26536  heiborlem10  26543  divrngidl  26652  prtlem10  26728  prtlem16  26732  prtlem19  26741  prtex  26743  prter3  26745  isnacs2  26774  rabrenfdioph  26889  expdiophlem1  27106  pw2f1ocnv  27122  pwfi2f1o  27251  numinfctb  27259  dfacbasgrp  27264  lindsmm  27289  islinds3  27295  islindf4  27299  islnr3  27310  subrgacs  27499  sdrgacs  27500  isdomn3  27514  dvconstbi  27542  rfcnpre3  27694  rfcnpre4  27695  stoweidlem59  27798  otthg  28079  f12dfv  28098  wlkcomp  28339  el2wlkonotot0  28404  2wot2wont  28418  usg2spthonot1  28422  2spot2iun2spont  28423  isrusgra  28442  vdn1frgrav2  28490  vdgn1frgrav2  28491  usgreg2spot  28530  sbc3org  28690  trsbc  28699  sbcssOLD  28701  bnj919  29210  bnj976  29222  bnj1542  29302  bnj150  29321  bnj151  29322  bnj607  29361  bnj852  29366  bnj873  29369  bnj938  29382  bnj1171  29443  bnj1388  29476  bnj1489  29499  equsalNEW7  29561  ax7w14lemAUX7  29743  islshpat  29889  lcvbr2  29894  lcvbr3  29895  lshpsmreu  29981  isat3  30179  hlrelat5N  30272  islpln5  30406  cdlemblem  30664  paddvaln0N  30672  paddval0  30681  cdlemefrs29bpre1  31268  cdlemefrs29cpre1  31269  cdlemg27b  31567  cdlemg33c  31579  cdlemg33e  31581  diaglbN  31927  cdlemm10N  31990  dicopelval2  32053  dicelval2N  32054  dihopelvalcpre  32120  dihglbcpreN  32172  dih1dimatlem  32201  dihatexv  32210  dvh4dimlem  32315  mapdpglem3  32547  hdmap14lem13  32755  hdmapglem7a  32802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator