Theorem syl6bb 539

Description: A syllogism inference from two biconditionals.

Hypotheses

Ref	Expression
syl6bb.1	⊢ (φ → (ψ ↔ χ))
syl6bb.2	⊢ (χ ↔ θ)

Assertion

Ref	Expression
syl6bb	⊢ (φ → (ψ ↔ θ))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		syl6bb.2	. . 3 ⊢ (χ ↔ θ)
3	2	a1i 8	. 2 ⊢ (φ → (χ ↔ θ))
4	1, 3	bitrd 531	1 ⊢ (φ → (ψ ↔ θ))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  syl6rbb 540  syl6bbr 541  3bitr3g 557  biantrurd 732  19.17 1085  19.33b 1128  2eu6 1494  abeq2d 1615  necon2bbid 1667  eqvinc 1929  eueq3 1965  reu7 1981  reu8 1982  sbcralt 2040  sbcralgf 2042  uniiunlem 2184  reldisj 2366  sbcsng 2490  eqsn 2539  eluniab 2579  elintab 2611  dfiun2g 2654  axsep2 2778  notzfaus 2815  moabex 2844  opcom 2877  opeqsn 2879  sotrieq2 2941  ordtri2 3010  ordtri4 3012  oneqmini 3024  ordtri2or 3067  reuxfr 3127  elpwunsn 3135  ralxp 3301  relop 3365  opelco2g 3380  opelcnvg 3387  reldm0 3418  relrn0 3443  iss 3487  asymref2 3532  xpnz 3551  dmsnop 3577  fncnv 3666  fvprc 3832  fnopfvb 3865  funopfvb 3867  fvelrnb 3871  funimass4 3874  fvopab3 3888  fvopabn 3897  eqfnfvALT 3910  eqfnfvf2 3912  fvreseq 3913  elrnopabg 3914  fsn 3948  fconstfv 3963  funiunfv 3980  dff13 3988  f1ocnvfv3 3997  isocnv 4010  isoini 4014  f1oiso 4018  eloprabg 4067  resoprab 4069  eqfnoprv 4076  oprabval6g 4093  oprvelrn 4100  caoprord2 4118  elopabi 4179  eloprabi 4180  elrnoprabg 4186  oevn0 4290  om00el 4343  omordlim 4344  omlimcl 4345  oeoa 4360  oeoe 4362  ecopoprsym 4451  th3qlem1 4455  dom2d 4545  mapsnen 4570  undom 4579  xpdom2 4583  pw2en 4587  ac6sfilem3 4590  0sdomg 4611  fodomr 4628  mapdom2 4641  mapxpen 4642  xpmapenlem5 4647  unfilem1 4694  abfii4 4707  fodomfi 4709  inf3lem1 4758  r1tr 4800  rankval2 4816  rankr1 4820  rankval3 4827  unbndrank 4829  r1pwcl 4833  bnd2 4870  aceq0 4876  aceq5lem4 4884  aceq5 4886  zfac 4891  ac6lem 4900  kmlem14 4924  iscard2 5004  alephord2 5026  cardaleph 5035  zfcndac 5125  ltexpi 5183  mulcmpblnq 5207  ordpipq 5210  ltsopq 5229  genpelv 5257  genpprecl 5258  genpnnp 5262  genpass 5266  distrlem1pr 5281  distrlem5pr 5285  prlem936a 5307  addcmpblnr 5335  ltsrpr 5340  ltsosr 5357  mulgt0sr 5368  map2psrpr 5374  ltresr 5412  axrnegex 5437  axrrecex 5438  pre-axltadd 5443  pre-axmulgt0 5444  negcon1 5564  negcon2 5565  xrrebnd 5722  lt0neg1 5822  lt0neg2 5823  le0neg1 5824  le0neg2 5825  divmul2 5860  reclt1 6043  recgt1 6044  infm3 6222  arch 6239  supxrbnd 6259  nn0ltp1le 6295  elznn0 6317  elnnz1 6323  elnn0nn 6339  zltp1le 6349  recnz 6362  dfuzi 6373  uzindOLD 6379  uzwo3lem2 6389  iooin 6498  elioo1 6504  elioo2 6505  elioo3g 6506  elioc1 6507  elico1 6508  elicc1 6509  elioo4g 6511  iooneg 6533  iccneg 6534  icounlem 6539  snunioolem 6541  ioojoin 6543  eluz1 6547  raluz 6569  rexuz 6571  elfz1 6598  elfz2 6600  elfzuzb 6604  elfzuz2 6614  elfz2nn0 6625  fzsuc 6636  fznn0 6647  seq1lem2 6675  exple1 6804  bernneq 6849  bernneqOLD 6850  sqr2irrlem3 6927  crulem 6937  creur 6943  creui 6944  abssubne0 7085  cvg2i 7125  dffsum 7201  fsumrev 7232  fsumshft 7234  clm1i 7280  clmnnsi 7287  climshfti 7307  climresi 7308  caucvgi 7366  caucvg3 7371  dfisum 7395  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  xpnnen 7711  infxpidmlem5 7768  infxpidmlem10 7773  istop2g 7809  isbasis2g 7824  isbasis3g 7825  eltg3 7838  tgss3 7850  elcls 7914  ntreq0 7918  islp 7954  islp2 7957  islpi 7959  cncnplem3 7986  cncnplem4 7987  ismet 8008  elbl 8048  blrn2 8052  blss 8063  metcnplem 8097  cncfmet 8116  dscmet 8129  lmbr2 8140  iscau2 8148  iscau5 8152  lmbrnns 8153  iscaunns 8155  metcn4 8182  isgrp 8254  issubg 8358  nvsubadd 8522  sspval 8636  isssp 8637  islno 8668  nmogtmnf 8687  nmounbi 8693  isblo 8697  ishmo 8726  ubthlem1 8787  spwmo 8918  pilem1 8938  sincosq1sgn 8971  sincosq2sgn 8972  efghgrpilem 8991  efif1lem5 9006  axgroth2 9050  grothinf 9053  hvmulcan2 9216  hire 9236  ocel 9430  ocsh 9432  chocunii 9448  shsel 9554  shscom 9559  shmodsi 9638  elspani 9742  adjsym 10039  eigorthi 10043  nmopgtmnf 10075  adjval2 10095  cnvadj 10096  hhlnoi 10106  elnlfn 10132  eleigvec 10161  nmop0h 10195  largei 10475  mdbr2 10504  mddmd2 10517  mdsl2i 10530  chrelat3 10579  atnem0 10585  atnem0OLD 10586  irredlem1 10599  sumdmdii 10624  sumdmdlem 10627  dmdbr5ati 10631  cdjreui 10641  elgiso 10683  uninqs 10730  elo 10733  domintreflem 10766  eloi 10817  isexid 10893  ismgm 10897  sbtpsines 11062  cnfilca 11088  rcfpfillem3 11091  rcfpfillem6 11094  plimfil 11103  altretoplem1 11142  ishomc 11244  ismona 11264  dfiin2g 11400  fictb 11423  omsublim 11448  compsublem 11487  compfipin0 11493  is1stc3 11530  isfne2 11542  isfne3 11543  comppfsc 11578  neibastop3 11585  ist0-2 11600  isfbas2 11622  fbasfip 11627  fbunfip 11631  isfillim 11676  flimfcn 11715  isfclus 11718  fcluscn 11731  fclsfcn 11744  inpreima 11793  respreima 11795  morex 11804  eqfnfv3 11819  fimax 11837  ac6gf 11841  indexa 11845  fimaxre 11856  fzpr 11866  fzm1 11867  sdc 11877  fsum00 11883  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  uptx 11978  heiborlem8 12018  heiborlem15 12025  rrncms 12075  rrntotbndlem1 12076  rrntotbnd 12078  isphtpy 12090  ishgrag 12195

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 145  df-an 223

Copyright terms: Public domain