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

Theorem syl6bbr 254
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 193 . 2  |-  ( ch  <->  th )
41, 3syl6bb 252 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr4g  279  bibi2i  304  mtt  329  nbn2  334  equsalhw  1730  equsal  1900  necon2abid  2503  eueq3  2940  sbcabel  3068  sbcel12g  3096  sbceqg  3097  sbcnel12g  3098  sbcne12g  3099  n0moeu  3467  reldisj  3498  r19.3rz  3545  r19.3rzv  3547  r19.9rzv  3548  ordelpss  4420  reusv2lem5  4539  ordsucun  4616  dflim3  4638  dfom2  4658  peano5  4679  rabxp  4725  elrng  4871  iss  4998  elimasni  5040  eliniseg  5042  xpcan  5112  xpcan2  5113  fcnvres  5418  dffv3  5521  funimass4  5573  fndmdif  5629  fneqeql  5633  funimass3  5641  dff4  5674  fconst4  5736  elunirnALT  5779  eqfnov  5950  caoftrn  6112  brtpos  6243  rntpos  6247  opiota  6290  f1ocnvfv3  6340  ordgt0ge1  6496  ondif2  6501  oelim2  6593  omabs  6645  iiner  6731  erinxp  6733  qliftfun  6743  ordunifi  7107  elfi2  7168  elfiun  7183  fifo  7185  noinfep  7360  cantnfrescl  7378  cantnf  7395  rankonidlem  7500  r1pwOLD  7518  pr2nelem  7634  cardalephex  7717  alephinit  7722  dfac5lem4  7753  cflim2  7889  cfsmolem  7896  compssiso  8000  fin1a2lem11  8036  itunisuc  8045  axdclem  8146  brdom6disj  8157  alephreg  8204  fpwwe2lem9  8260  pwfseqlem3  8282  pwfseqlem4  8284  indpi  8531  nqereu  8553  ordpinq  8567  ltanq  8595  ltmnq  8596  suplem2pr  8677  map2psrpr  8732  ssxr  8892  letri3  8907  leltne  8911  ltneg  9274  leneg  9277  suprnub  9717  negiso  9730  infmrgelb  9734  elnnnn0  10007  nn0sub  10014  zrevaddcl  10063  znnsub  10064  znn0sub  10065  prime  10092  eluz2  10236  indstr  10287  eluz2b1  10289  qrevaddcl  10338  rpneg  10383  xrleltne  10479  dfle2  10481  dflt2  10482  xrletri3  10486  supxrleub  10645  infmxrgelb  10653  ixxin  10673  iccid  10701  elicopnf  10739  iccsplit  10768  fzsplit2  10815  fzsn  10833  fzpr  10840  uzsplit  10855  om2uzf1oi  11016  lt2sqi  11192  le2sqi  11193  hashsdom  11363  hashf1lem1  11393  fz1isolem  11399  ccatlcan  11464  ccatrcan  11465  cnpart  11725  limsuplt  11953  rlimresb  12039  mertenslem2  12341  sadadd2lem2  12641  saddisjlem  12655  bitsuz  12665  gcddiv  12728  algcvgblem  12747  isprm2lem  12765  isprm3  12767  isprm5  12791  prmreclem5  12967  vdwapun  13021  vdwmc2  13026  ramcl  13076  pwsle  13391  ismre  13492  mreacs  13560  acsfn  13561  iscatd2  13583  cidpropd  13613  oppcsect2  13677  isfunc  13738  setcinv  13922  tosso  14142  ipodrsfi  14266  acsfiindd  14280  imasmnd2  14409  submacs  14442  imasgrp2  14610  issubg  14621  subgacs  14652  eqgval  14666  gaorber  14762  isslw  14919  sylow2alem2  14929  sylow2a  14930  sylow3lem6  14943  efgcpbllemb  15064  prmcyg  15180  gsum2d2lem  15224  gsumcom2  15226  subgdmdprd  15269  dprd2d2  15279  pgpfac1lem2  15310  pgpfac1lem4  15313  imasrng  15402  drngmulne0  15534  lssle0  15707  lssacs  15724  lssats2  15757  lvecvsn0  15862  islpir  16001  isnzr2  16015  zndvds  16503  znleval  16508  znleval2  16509  eltg2b  16697  discld  16826  opnssneib  16852  cldlp  16881  restbas  16889  leordtvallem1  16940  leordtvallem2  16941  ssidcn  16985  cnprest2  17018  lmss  17026  perfcls  17093  cmpfi  17135  1stccnp  17188  subislly  17207  hausmapdom  17226  iskgen3  17244  kgencn  17251  ptpjpre1  17266  xkoccn  17313  txrest  17325  txlm  17342  txkgen  17346  xkopt  17349  xkoinjcn  17381  qtopcn  17405  kqfeq  17415  isr0  17428  fbfinnfr  17536  trfbas  17539  fbunfip  17564  ufileu  17614  cfinufil  17623  fmid  17655  txflf  17701  fclsrest  17719  alexsubALT  17745  tsmsres  17826  bldisj  17955  xmeter  17979  dscopn  18096  bl2ioo  18298  isphtpc  18492  tchcph  18667  lmmbr2  18685  lmmbrf  18688  iscau2  18703  iscauf  18706  caucfil  18709  metcld  18731  metcld2  18732  bcthlem1  18746  bcthlem4  18749  cldcss2  18806  ovolgelb  18839  ovoliunlem1  18861  ismbfcn  18986  mbfmax  19004  mbfimaopnlem  19010  i1faddlem  19048  i1fmullem  19049  i1fres  19060  i1fpos  19061  itg1climres  19069  xrge0f  19086  itgresr  19133  iblcnlem1  19142  limcun  19245  dvres  19261  itgsubst  19396  mdegmullem  19464  ply1remlem  19548  plyremlem  19684  vieta1  19692  ulmcau  19772  sineq0  19889  coseq1  19890  ang180lem3  20109  cubic  20145  atandm  20172  atandm2  20173  atandm3  20174  rlimcnp  20260  rlimcnp2  20261  vmappw  20354  dchrelbas3  20477  dchrelbas4  20482  dchrsum2  20507  bposlem6  20528  dchrisumlem3  20640  pntleml  20760  elghom  21030  nmoolb  21349  nmlno0lem  21371  ubthlem1  21449  ocsh  21862  shle0  22021  eigrei  22414  adjeu  22469  nmoplb  22487  nmfnlb  22504  eleigvec2  22538  nmlnop0iALT  22575  cnlnadjlem5  22651  adjbdln  22663  jplem2  22849  cvbr2  22863  mdsl2bi  22903  chrelat3  22951  fzsplit3  23031  ballotlemfc0  23051  ballotlemfcc  23052  ofrn2  23207  funcnvmpt  23235  funcnv5mpt  23236  gtiso  23241  xrdifh  23273  unitdivcld  23285  lmxrge0  23375  xrge0tsmsbi  23383  eldifpr  23394  eldiftp  23395  dstfrvunirn  23675  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem9  23730  kur14  23747  iscvm  23790  eupath2lem2  23902  dfpo2  24112  fundmpss  24122  dfon2  24148  elpredg  24178  preduz  24200  tfrALTlem  24276  nofulllem1  24356  nofulllem2  24357  dfbigcup2  24439  dffun10  24453  brimg  24476  dfrdg4  24488  brbtwn2  24533  axsegconlem6  24550  axsegcon  24555  ax5seg  24566  axpasch  24569  axeuclid  24591  axcontlem4  24595  cgr3permute3  24670  segletr  24737  segleantisym  24738  seglelin  24739  splint  25048  inttpemp  25139  iint  25612  algi  25727  rdmob  25748  vtarsuelt  25895  pdiveql  26168  abhp2  26175  bhp2a  26176  fneval  26287  locfindis  26305  neibastop3  26311  eltail  26323  filnetlem4  26330  caures  26476  heiborlem3  26537  heiborlem10  26544  divrngidl  26653  prtlem10  26733  prtlem16  26737  prtlem19  26746  prtex  26748  prter3  26750  isnacs2  26781  rabrenfdioph  26897  expdiophlem1  27114  pw2f1ocnv  27130  pwfi2f1o  27260  numinfctb  27268  dfacbasgrp  27273  lindsmm  27298  islinds3  27304  islindf4  27308  islnr3  27319  subrgacs  27508  sdrgacs  27509  isdomn3  27523  dvconstbi  27551  rfcnpre3  27704  rfcnpre4  27705  stoweidlem59  27808  mpt2xopovel  28086  nbgrael  28141  nbcusgra  28159  sbc3org  28295  trsbc  28304  sbcssOLD  28306  bnj919  28797  bnj976  28809  bnj1542  28889  bnj150  28908  bnj151  28909  bnj607  28948  bnj852  28953  bnj873  28956  bnj938  28969  bnj1171  29030  bnj1388  29063  bnj1489  29086  islshpat  29207  lcvbr2  29212  lcvbr3  29213  lshpsmreu  29299  isat3  29497  hlrelat5N  29590  islpln5  29724  cdlemblem  29982  paddvaln0N  29990  paddval0  29999  cdlemefrs29bpre1  30586  cdlemefrs29cpre1  30587  cdlemg27b  30885  cdlemg33c  30897  cdlemg33e  30899  diaglbN  31245  cdlemm10N  31308  dicopelval2  31371  dicelval2N  31372  dihopelvalcpre  31438  dihglbcpreN  31490  dih1dimatlem  31519  dihatexv  31528  dvh4dimlem  31633  mapdpglem3  31865  hdmap14lem13  32073  hdmapglem7a  32120
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