HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syl6bb 534
Description: A syllogism inference from two biconditionals.
Hypotheses
Ref Expression
syl6bb.1 |- (ph -> (ps <-> ch))
syl6bb.2 |- (ch <-> th)
Assertion
Ref Expression
syl6bb |- (ph -> (ps <-> th))
Proof of Theorem syl6bb
StepHypRef Expression
1 syl6bb.1 . 2 |- (ph -> (ps <-> ch))
2 syl6bb.2 . . 3 |- (ch <-> th)
32a1i 8 . 2 |- (ph -> (ch <-> th))
41, 3bitrd 526 1 |- (ph -> (ps <-> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  syl6rbb 535  syl6bbr 536  3bitr3g 552  biantrurd 725  19.17 1045  19.33b 1088  2eu6 1447  abeq2d 1564  necon2bbid 1615  eqvinc 1874  eueq3 1910  reu7 1925  reu8 1926  sbcralt 1980  sbcralgf 1982  uniiunlem 2122  reldisj 2303  eqsn 2465  eluniab 2503  elintab 2534  dfiun2g 2576  axsep2 2694  notzfaus 2731  sbcsng 2743  moabex 2756  opeqsn 2791  sotrieq2 2853  reuxfr 2894  elpwunsn 2902  ordtri2 2972  ordtri4 2974  oneqmini 3007  ordtri2or 3067  ralxp 3208  relop 3265  opelcog 3279  opelcnvg 3285  dmsnop 3317  reldm0 3320  relrn0 3342  iss 3381  asymref2 3424  asymref2OLD 3426  xpnz 3452  fncnv 3547  fvprc 3706  fnopfvb 3739  funopfvb 3741  fvelrnb 3745  funimass4 3748  fvopab3 3762  fvopabn 3771  eqfnfvf 3783  elrnopabg 3785  fsn 3819  fconstfv 3834  funiunfv 3851  f1fv 3859  f1ocnvfv3 3868  isocnv 3881  isoini 3885  f1oiso 3889  eloprabg 3992  resoprab 3994  eqfnoprval 4001  oprabval6g 4017  oprvalelrn 4024  caoprord2 4043  2ndconst 4081  elopabi 4101  eloprabi 4102  elrnoprabg 4108  oevn0 4138  om00el 4191  omordlim 4192  omlimcl 4193  ecopoprsym 4294  th3qlem1 4298  dom2d 4385  mapsnen 4410  undom 4418  xpdom2 4422  pw2en 4426  0sdomg 4446  fodomr 4463  mapdom2 4474  mapxpen 4475  xpmapenlem5 4480  unfilem1 4524  abfii4 4538  fodomfi 4540  inf3lem1 4585  r1tr 4626  rankval2 4642  rankr1 4646  rankval3 4653  unbndrank 4655  r1pwcl 4659  bnd2 4696  aceq0 4702  aceq5lem4 4710  aceq5 4712  axac 4717  ac6lem 4726  kmlem14 4750  iscard2 4826  alephord2 4848  cardaleph 4857  zfcndac 4943  ltexpi 5001  mulcmpblnq 5025  ordpipq 5028  ltsopq 5047  genpelv 5075  genpprecl 5076  genpnnp 5080  genpass 5084  distrlem1pr 5099  distrlem5pr 5103  prlem936a 5125  addcmpblnr 5153  ltsrpr 5158  ltsosr 5175  mulgt0sr 5186  map2psrpr 5192  ltresr 5230  axrnegex 5255  axrrecex 5256  pre-axltadd 5261  pre-axmulgt0 5262  negcon1t 5382  negcon2t 5383  xrrebndt 5541  lt0neg1t 5641  lt0neg2t 5642  le0neg1t 5643  le0neg2t 5644  divmul2t 5677  reclt1t 5846  recgt1t 5847  infm3 6001  arch 6018  supxrbnd 6038  nn0ltp1let 6074  elznn0 6096  elnnz1 6102  elnn0nn 6118  zltp1let 6128  recnzt 6138  dfuz 6150  uzindOLD 6156  uzwo3lem2 6165  seq1lem2 6247  iooint 6309  elioo1t 6315  elioo2t 6316  elioo3g 6317  elioo4g 6318  elioc1t 6319  elico1t 6320  elicc1t 6321  ioonegt 6339  iccnegt 6340  icounlem 6345  snunioolem 6347  eluz1t 6352  raluz 6374  rexuz 6376  elfz1t 6402  elfz2t 6404  elfzuzb 6408  elfzuz2t 6418  elfz2nn0t 6427  fznn0t 6448  exple1t 6538  bernneq 6583  sqr2irrlem3 6656  crulem 6666  creur 6673  creui 6674  abssubne0t 6820  cvg2 6859  dffsum 6936  fsumrev 6967  fsumshft 6969  clm1 7015  clmnns 7022  climshft 7041  climres 7042  caucvg 7099  caucvg3t 7104  dfisum 7127  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  xpnnen 7441  infxpidmlem5 7499  infxpidmlem10 7504  istop2g 7539  isbasis2g 7554  isbasis3g 7555  eltg3t 7568  tgss3t 7580  elcls 7646  ntreq0 7650  islp 7685  islp2 7688  islpi 7690  cncnplem3 7715  cncnplem4 7716  ismet 7737  elbl 7778  blrn2 7782  blss 7793  metcnplem 7825  cncfmet 7844  dscmet 7856  lmbr2 7867  iscau2 7875  iscau5 7878  metcn4 7905  isgrp 7975  issubg 8053  nvsubadd 8215  sspval 8316  isssp 8317  islno 8348  nmogtmnf 8365  nmounbi 8371  isblo 8374  ubthlem1 8460  spwmo 8580  pilem1 8590  sincosq1sgn 8621  sincosq2sgn 8622  efghgrpilem 8634  efif1lem5 8649  axgroth2 8717  grothinf 8720  hvmulcan2t 8861  hiret 8881  ocelt 9070  ocsh 9072  chocuni 9088  shselt 9193  shscomt 9198  shmods 9277  elspan 9381  adjsymt 9676  eigorth 9680  nmopgtmnf 9712  adjval2t 9732  cnvadj 9733  hhlno 9743  elnlfnt 9768  eleigvect 9797  nmop0h 9831  large 10104  mdbr2 10133  mddmd 10144  mdsl2 10157  chrelat3t 10206  atnem0 10212  irredlem1 10225  sumdmdi 10249  sumdmdlem 10252  dmdbr5at 10255  cdjreu 10264  elgiso 10303  uninqs 10342  elo 10345  cnfilca 10451  eloi 10503  ishomc 10561  ismona 10579  ishgrag 10605
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain