Theorem syl5bb 283

Description: A syllogism inference from two biconditionals. This is in the process of being renamed to bitrid 282 (New usages should use bitrid 282). (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
syl5bb.1	⊢ (𝜑 ↔ 𝜓)
syl5bb.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5bb	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3		syl5bb.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	bitrd 278	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  isclwlkupgr  28155  iswwlksnx  28214  wwlksnextwrd  28271  wwlksnextproplem3  28285  2pthon3v  28317  umgr2wlk  28323  elwwlks2on  28333  elwwlks2  28340  elwspths2spth  28341  clwwlknclwwlkdif  28352  clwlkclwwlk  28375  clwlkclwwlk2  28376  clwwlkn1  28414  clwwlkn2  28417  clwwlkwwlksb  28427  eclclwwlkn1  28448  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknonel  28468  clwwlknon1  28470  clwwlknun  28485  1pthon2v  28526  uhgr3cyclex  28555  isconngr  28562  isconngr1  28563  eupthres  28588  eupth2lems  28611  frgr0v  28635  frgr3vlem2  28647  fusgr2wsp2nb  28707  extwwlkfab  28725  numclwwlk1lem2foa  28727  numclwwlk1lem2fo  28731  isvclem  28948  isnvlem  28981  isphg  29188  isph  29193  phoeqi  29228  ubthlem3  29243  minvecolem5  29252  minvecolem6  29253  minvecolem7  29254  hhph  29549  issh3  29590  nmopub  30279  nmfnleub  30296  adjeq  30306  adjvalval  30308  elunop2  30384  lnophm  30390  nmcexi  30397  cnlnadjlem5  30442  cnlnadjeui  30448  adjbd1o  30456  jpi  30641  mddmd2  30680  chrelati  30735  chrelat2i  30736  cvexchlem  30739  dmdbr5ati  30793  cdjreui  30803  cdj3i  30812  elunsn  30867  disjunsn  30942  opeldifid  30947  fcoinvbr  30956  brabgaf  30957  opabdm  30960  opabrn  30961  iunsnima  30967  nfpconfp  30976  elimampt  30982  abfmpunirn  30998  fmptcof2  31003  funcnvmpt  31013  funcnv5mpt  31014  suppiniseg  31029  ressupprn  31033  brprop  31039  f1od2  31065  resf1o  31074  fpwrelmap  31077  iocinioc2  31109  eliccioo  31214  wrdt2ind  31234  posrasymb  31252  mgccnv  31286  isslmd  31464  nsgqusf1olem3  31609  prmidl0  31635  fedgmullem2  31720  smatrcl  31755  rspectopn  31826  pstmxmet  31856  prsdm  31873  prsrn  31874  ordtconnlem1  31883  xrmulc1cn  31889  ispisys2  32130  elcarsg  32281  eulerpartlemmf  32351  isrrvv  32419  reprinrn  32607  tgoldbachgt  32652  bnj976  32766  bnj944  32927  bnj1173  32991  bnj1321  33016  bnj1373  33019  bnj1417  33030  fineqvrep  33073  lfuhgr  33088  revwlk  33095  usgrgt2cycl  33101  subfacp1lem3  33153  subfacp1lem6  33156  subfacp1  33157  txpconn  33203  sconnpi1  33210  resconn  33217  cvmscbv  33229  cvmsval  33237  cvmlift2lem13  33286  cvmlift3lem2  33291  cvmlift3  33299  goeleq12bg  33320  satfvsucsuc  33336  satfbrsuc  33337  fmlafvel  33356  satffunlem2lem1  33375  satefvfmla1  33396  mclsrcl  33532  fnssintima  33685  imaeqsexv  33699  br8  33732  br6  33733  br4  33734  elintfv  33747  fv1stcnv  33760  fv2ndcnv  33761  distel  33788  frxp2  33800  xpord2pred  33801  frxp3  33806  xpord3pred  33807  poseq  33811  wsuclem  33828  sltsolem1  33887  nosupdm  33916  nosupbnd1lem4  33923  slenlt  33964  sleloe  33966  eqscut2  34009  madeval2  34046  elold  34062  imageval  34241  funpartfv  34256  dfrdg4  34262  altopthg  34278  altopthbg  34279  brcolinear2  34369  lineext  34387  brsegle  34419  seglelin  34427  broutsideof2  34433  isfne4  34538  isfne2  34540  isfne3  34541  fneval  34550  topfneec  34553  neibastop2lem  34558  neibastop2  34559  neifg  34569  filnetlem4  34579  onsuct0  34639  bj-19.41t  34965  bj-sbievwd  34973  bj-elgab  35136  bj-tagcg  35184  bj-projval  35195  bj-restuni  35277  opelopabd  35321  opelopabb  35322  brabd0  35327  bj-opelid  35336  bj-ideqg  35337  bj-opelidres  35341  bj-ideqg1  35344  bj-elid6  35350  bj-isvec  35467  bj-isclm  35471  bj-isrvecd  35478  csboprabg  35510  csbmpo123  35511  topdifinffinlem  35527  isbasisrelowllem1  35535  isbasisrelowllem2  35536  rdgeqoa  35550  csbfinxpg  35568  nlpineqsn  35588  uncov  35767  tan2h  35778  matunitlindf  35784  ptrest  35785  poimirlem2  35788  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  cnambfre  35834  itg2addnclem2  35838  fdc  35912  heibor1  35977  rrncmslem  35999  rrnheibor  36004  opidonOLD  36019  issmgrpOLD  36030  ismndo  36039  isrngo  36064  isdivrngo  36117  isfldidl2  36236  isdmn3  36241  releleccnv  36404  releccnveq  36405  brcnvep  36412  elecres  36420  eleccnvep  36424  ideq2  36450  extid  36453  relcnveq3  36463  eqres  36482  brrabga  36483  ecin0  36491  alrmomodm  36498  brxrn  36511  brxrn2  36512  elecxrn  36523  br1cnvxrn2  36529  elec1cnvxrn2  36530  br1cossinres  36572  br1cossxrnres  36573  eldmcoss  36583  elrels2  36611  elrelscnveq3  36616  br1cnvssrres  36630  brcnvssr  36631  dfrefrels2  36638  dfcnvrefrels2  36651  dfsymrels2  36666  elrefsymrelsrel  36692  dftrrels2  36696  erim2  36796  eldisjs5  36844  prtlem13  36889  prter3  36903  lrelat  37035  islshpat  37038  lshpsmreu  37130  lkrpssN  37184  cmtvalN  37232  omllaw2N  37265  cvrval  37290  cvrval2  37295  cvlsupr3  37365  3dim0  37478  islln2  37532  islpln5  37556  islpln2  37557  islpln2ah  37570  islvol5  37600  islvol2  37601  4atlem11  37630  pmapglbx  37790  cdleme18d  38316  cdlemefrs29bpre0  38417  cdlemb3  38627  cdlemg33b  38728  cdlemkid3N  38954  cdlemkid4  38955  dvhb1dimN  39007  dia11N  39069  cdlemm10N  39139  dib11N  39181  dib1dim  39186  dibglbN  39187  diblsmopel  39192  dihopelvalcpre  39269  dih11  39286  dihmeetlem4preN  39327  dihmeetlem13N  39340  lcfrvalsnN  39562  lcfrlem9  39571  lcf1o  39572  mapdval4N  39653  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  hdmap1fval  39817  hdmapfval  39848  hdmapglem7a  39948  hlhillcs  39983  elab2gw  40173  19.9dev  40185  frlmfielbas  40238  fsuppind  40286  fsuppssindlem2  40288  addsubeq4com  40315  prjspreln0  40455  ellz1  40596  lzunuz  40597  fz1eqin  40598  diophrex  40604  rexrabdioph  40623  rexfrabdioph  40624  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  fzneg  40811  expdioph  40852  wepwsolem  40874  fnwe2lem2  40883  islmodfg  40901  kercvrlsm  40915  scottabf  41865  pm10.52  41990  iotasbc  42044  pm14.122a  42047  pm14.122b  42048  pm14.123a  42050  rusbcALT  42064  fvsb  42077  trsbc  42167  wessf1ornlem  42729  imassmpt  42817  limcperiod  43176  limsupre  43189  dvbdfbdioo  43478  stoweidlem34  43582  fourierdlem108  43762  fourierdlem110  43764  etransc  43831  funressnfv  44548  dfafn5a  44663  ndfatafv2nrn  44724  afv2ndefb  44727  dfatsnafv2  44755  dfatdmfcoafv2  44757  dfatco  44759  afv2fv0xorb  44770  readdcnnred  44806  resubcnnred  44807  recnmulnred  44808  cndivrenred  44809  elfz2z  44818  el1fzopredsuc  44828  elsetpreimafvb  44847  iccelpart  44896  ichan  44918  ichal  44929  reupr  44985  lighneallem2  45069  dfeven2  45112  gbowge7  45226  sbgoldbwt  45240  isupwlk  45309  uspgrsprfo  45321  ismhm0  45370  inclfusubc  45436  isrnghm  45461  rnghmval2  45464  uzlidlring  45498  lidldomnnring  45499  zrninitoringc  45640  opeliun2xp  45679  snlindsntor  45823  elbigo2  45909  resum2sqorgt0  46066  rrx2pnedifcoorneor  46073  rrx2plord  46077  rrx2plordisom  46080  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2linest2  46101  itsclc0b  46129  itsclinecirc0in  46132  inlinecirc02plem  46143  fvconstr  46194  fvconstrn0  46195  opndisj  46207  clddisj  46208  i0oii  46224  io1ii  46225  isthincd2lem1  46319  functhinc  46337  gte-lte  46437  gt-lt  46438