Theorem syl5bb 285

Description: A syllogism inference from two biconditionals. (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 281	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl5rbb  286  syl5bbr  287  3bitr4g  316  imim21b  397  ifpfal  1069  norass  1533  cad0  1618  ax12wdemo  2139  eu6lem  2658  abbi  2888  necon3abid  3052  necon3bid  3060  ralxpxfr2d  3639  ceqsrexv  3649  ceqsrex2v  3651  elab2g  3668  elrabf  3676  elrab3t  3679  eueq2  3701  eqreu  3720  reu8  3724  ru  3771  sbcralt  3855  sbcabel  3861  sbcel1g  4365  sbcel2  4367  csbnestgfw  4371  csbnestgf  4376  sbccsb2  4386  2nreu  4393  disjpss  4410  sbcssg  4463  2reu4lem  4465  rexsngf  4610  reusngf  4612  ralprgf  4630  rexprgf  4631  reuprg0  4638  difsn  4731  preq2b  4778  opthpr  4782  preqsnd  4789  csbopg  4821  ralunsn  4824  csbuni  4867  dfiin2g  4957  iunxsng  5012  iunxsngf  5014  elpwuni  5027  disjxun  5064  sbcbr12g  5122  opthneg  5373  otthg  5377  opeqsng  5393  snopeqop  5396  opelopabt  5419  opelopabga  5420  brabga  5421  opelopabgf  5427  csbmpt12  5444  rbropapd  5449  dfid3  5462  frirr  5532  wereu2  5552  opeliunxp  5619  posn  5637  sosn  5638  frsn  5639  brab2a  5644  opbrop  5648  csbcnvgALT  5755  dmopabelb  5785  elrnmpt1  5830  elrnmptg  5831  opelres  5859  eliniseg2  5969  poleloe  5991  xpdifid  6025  cnvpo  6138  reu3op  6143  elpred  6161  ordtri4  6228  oneqmini  6242  elsucg  6258  elsuc2g  6259  sbcfung  6379  dffun8  6383  fncnv  6427  fununi  6429  fnssresb  6469  fnimaeq0  6481  csbfv12  6713  dffn5  6724  funimass4  6730  feqmptdf  6735  fnsnfv  6743  dmfco  6757  fndmdif  6812  fvimacnvi  6822  fvimacnvALT  6827  unpreima  6833  respreima  6836  fmptco  6891  fressnfv  6922  fmptsnd  6931  fnnfpeq0  6940  tpres  6963  elunirn  7010  dff13  7013  f12dfv  7030  f13dfv  7031  fliftel  7062  isoini  7091  f1oiso  7104  riotaeqimp  7140  fnbrovb  7205  eloprabga  7261  resoprab2  7271  elrnmpores  7288  ralrnmpo  7289  ovid  7291  ov  7294  ovg  7313  ofrfval2  7427  dfwe2  7496  ssonprc  7507  ordpwsuc  7530  dfom2  7582  f1oweALT  7673  el2xptp0  7736  releldmdifi  7744  fmpox  7765  ovmptss  7788  1stconst  7795  2ndconst  7796  fnsuppres  7857  brtpos2  7898  mpocurryd  7935  dfsmo2  7984  rdglim2  8068  seqomlem2  8087  omeu  8211  oeeui  8228  brdifun  8318  eqerlem  8323  brecop  8390  erovlem  8393  eceqoveq  8402  mapsnd  8450  ixpsnval  8464  mptelixpg  8499  xpsnen  8601  xpdom2  8612  omxpenlem  8618  xpf1o  8679  mapunen  8686  onfin  8709  fimaxg  8765  fodomfib  8798  fofinf1o  8799  fipreima  8830  supub  8923  infglb  8954  infglbb  8955  fiming  8962  fiinfg  8963  ordtypecbv  8981  ordtypelem3  8984  ordtypelem9  8990  hartogslem1  9006  wofib  9009  wemapsolem  9014  wemapso2lem  9016  noinfep  9123  cantnf  9156  rankbnd2  9298  domtri2  9418  infxpenc2  9448  fseqdom  9452  acni2  9472  dfac9  9562  cfeq0  9678  cfsuc  9679  cflim3  9684  cfslb  9688  cofsmo  9691  enfin2i  9743  isfin3ds  9751  isf33lem  9788  fin1a2lem5  9826  axdc2lem  9870  zorn2g  9925  fodomb  9948  brdom7disj  9953  brdom6disj  9954  iundom2g  9962  cfpwsdom  10006  elgch  10044  fpwwe2cbv  10052  fpwwecbv  10066  pwfseqlem3  10082  pwfseqlem4a  10083  pwfseqlem4  10084  ltpiord  10309  nlt1pi  10328  nqereu  10351  addclprlem1  10438  1idpr  10451  reclem3pr  10471  ltsosr  10516  map2psrpr  10532  supsrlem  10533  axrrecex  10585  xrlenlt  10706  eqlei2  10751  addsubeq4  10901  renegcli  10947  lesub0  11157  wloglei  11172  conjmul  11357  rereccl  11358  infm3  11600  supaddc  11608  supadd  11609  supmul1  11610  supmullem1  11611  supmullem2  11612  supmul  11613  creui  11633  nndiv  11684  elznn0  11997  prime  12064  eqreznegel  12335  zsupss  12338  rebtwnz  12348  negelrp  12423  ltxr  12511  elixx3g  12752  ixxun  12755  ioo0  12764  ico0  12785  ioc0  12786  icc0  12787  difreicc  12871  divelunit  12881  iccf1o  12883  elfz2  12900  fzn  12924  fznn  12976  fzshftral  12996  nelfzo  13044  fzosplitsni  13149  om2uzisoi  13323  rabssnn0fi  13355  mptnn0fsupp  13366  sq11i  13555  hashsdom  13743  fi1uzind  13856  wrdval  13865  csbwrdg  13895  wrd2ind  14085  s2f1o  14278  cjreb  14482  rexfiuz  14707  cau3lem  14714  rlim2  14853  ello12  14873  ello1mpt  14878  elo12  14884  o1lo1  14894  lo1resb  14921  o1resb  14923  o1compt  14944  caucvgb  15036  pwm1geoserOLD  15225  mertens  15242  ruclem12  15594  divides  15609  dvdsabseq  15663  odd2np1  15690  oddm1even  15692  sumodd  15739  divalgmod  15757  modremain  15759  sadadd2lem2  15799  gcdcllem2  15849  bezoutlem2  15888  bezoutlem3  15889  bezoutlem4  15890  isprm2  16026  isprm3  16027  dvdsnprmd  16034  oddprmdvds  16239  prmreclem2  16253  prmreclem5  16256  prmreclem6  16257  4sqlem2  16285  4sqlem12  16292  vdwmc  16314  vdwpc  16316  vdwlem6  16322  vdwlem10  16326  vdwnn  16334  ramval  16344  0ram  16356  prdsleval  16750  pwsle  16765  imasleval  16814  xpsfrnel2  16837  xpsle  16852  isacs2  16924  mreacs  16929  acsfn  16930  iscatd2  16952  catpropd  16979  ciclcl  17072  cicrcl  17073  isssc  17090  evlfcl  17472  uncfcurf  17489  pltval  17570  lublecllem  17598  tosso  17646  oduleg  17742  oduclatb  17754  posglbmo  17757  isipodrs  17771  odudlatb  17806  gsumvalx  17886  elefmndbas  18038  sgrp2rid2  18091  grplmulf1o  18173  grplactcnv  18202  elnmz  18315  eqgid  18332  isghm  18358  ghmeqker  18385  resscntz  18462  symg1bas  18519  pgrpsubgsymgbi  18536  symgfixelq  18561  f1omvdconj  18574  odmulgeq  18684  sylow3lem3  18754  sylow3lem6  18757  efgval2  18850  efgsdm  18856  efgrelexlema  18875  efgcpbllemb  18881  iscyggen2  19000  cyggenod  19003  gsummptfzcl  19089  eldprd  19126  dprdf11  19145  dprddisj2  19161  pgpfac1lem2  19197  pgpfac1  19202  srg1zr  19279  drngid2  19518  issubrg  19535  sdrgacs  19580  islmod  19638  aspval2  20127  psrbag  20144  cply1coe0bi  20468  zndvds  20696  znleval  20701  iunocv  20825  pjfval2  20853  pjdm2  20855  dsmmelbas  20883  ellspd  20946  islindf  20956  islindf4  20982  istopg  21503  basgen2  21597  isclo  21695  mretopd  21700  isnei  21711  isperf3  21761  restdis  21786  neitr  21788  restcls  21789  restlp  21791  restperf  21792  iscn  21843  iscnp  21845  lmbr2  21867  lmbrf  21868  ordtt1  21987  cmpsub  22008  hauscmplem  22014  cmpfi  22016  dfconn2  22027  1stcelcls  22069  1stccn  22071  nllyi  22083  subislly  22089  dissnlocfin  22137  elkgen  22144  ptpjpre1  22179  ptuni2  22184  ptclsg  22223  ptcnplem  22229  txcn  22234  hausdiag  22253  txhaus  22255  txkgen  22260  xkoptsub  22262  cnmpt21  22279  elqtop  22305  tgqtop  22320  r0cld  22346  elfg  22479  fbasrn  22492  trfil2  22495  trfil3  22496  fin1aufil  22540  elfm2  22556  elfm3  22558  flimopn  22583  fbflim  22584  flfnei  22599  flftg  22604  cnpflf2  22608  txflf  22614  fclsbas  22629  alexsubALTlem4  22658  cnextfvval  22673  snclseqg  22724  tgphaus  22725  tsmsfbas  22736  tsmssubm  22751  utopsnneip  22857  prdsxmetlem  22978  imasdsf1olem  22983  xpsdsval  22991  blres  23041  isxms2  23058  metcnp  23151  txmetcnp  23157  txmetcn  23158  metustel  23160  metuel2  23175  dscopn  23183  isngp4  23221  cnblcld  23383  metnrmlem1a  23466  icoopnst  23543  iocopnst  23544  elpi1  23649  isclmp  23701  isncvsngp  23753  lmmbr2  23862  cfil3i  23872  caucfil  23886  iscmet3  23896  lmclim  23906  metcld2  23910  bcthlem4  23930  minveclem3b  24031  minveclem6  24037  minveclem7  24038  ivthle  24057  ivthle2  24058  evthicc2  24061  ovolfioo  24068  ovolficc  24069  ovolgelb  24081  dyadmax  24199  subopnmbl  24205  ismbf3d  24255  mbfimaopnlem  24256  mbfimaopn2  24258  mbfaddlem  24261  mbfsup  24265  mbfinf  24266  i1f1lem  24290  i1fmulclem  24303  itg1climres  24315  mbfi1fseqlem4  24319  itg2monolem1  24351  itg2gt0  24361  isibl  24366  iblcnlem1  24388  ellimc2  24475  dvcnvrelem1  24614  itgsubst  24646  mdegleb  24658  fta1glem2  24760  quotval  24881  vieta1lem1  24899  vieta1lem2  24900  ulm2  24973  ulmcaulem  24982  ulmcau  24983  radcnvlt1  25006  sineq0  25109  cos11  25117  recosf1o  25119  efopn  25241  cxpeq  25338  mcubic  25425  birthdaylem3  25531  rlimcnp  25543  xrlimcnp  25546  eldmgm  25599  dmgmaddn0  25600  lgamgulmlem6  25611  wilth  25648  isppw  25691  isppw2  25692  mumullem2  25757  sqff1o  25759  dvdsmulf1o  25771  fsumvma  25789  fsumvma2  25790  vmasum  25792  chpchtsum  25795  lgsne0  25911  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1a  25967  addsq2reu  26016  2sqreu  26032  2sqreunn  26033  2sqreult  26034  2sqreunnlt  26036  dchrmusumlema  26069  rpvmasum2  26088  dchrisum0lema  26090  pntibndlem3  26168  pntlemi  26180  pntleml  26187  pnt3  26188  trgcgrg  26301  tgcgr4  26317  colcom  26344  colrot1  26345  ltgov  26383  hlcomb  26389  lncom  26408  mirreu3  26440  isperp  26498  perpcom  26499  iscgra  26595  isinag  26624  brbtwn  26685  brcgr  26686  brbtwn2  26691  colinearalg  26696  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  elntg2  26771  edgiedgb  26839  isuhgr  26845  isushgr  26846  isupgr  26869  isumgr  26880  isuspgr  26937  isusgr  26938  uhgr0v0e  27020  isfusgrf1  27102  opfusgr  27105  usgr1v0e  27108  dfnbgr3  27120  nbuhgr2vtx1edgb  27134  edgnbusgreu  27149  nbusgredgeu0  27150  isuvtx  27177  cusgruvtxb  27204  cplgr3v  27217  cusgrsizeinds  27234  vtxdg0v  27255  vtxd0nedgb  27270  vtxduhgr0nedg  27274  vtxdusgr0edgnelALT  27278  iswlk  27392  wlk1walk  27420  upgr2wlk  27450  upgristrl  27484  2pthnloop  27512  usgr2pthlem  27544  isclwlke  27558  isclwlkupgr  27559  iswwlksnx  27618  wwlksnextwrd  27675  wwlksnextproplem3  27690  2pthon3v  27722  umgr2wlk  27728  elwwlks2on  27738  elwwlks2  27745  elwspths2spth  27746  clwwlknclwwlkdif  27757  clwlkclwwlk  27780  clwlkclwwlk2  27781  clwwlkn1  27819  clwwlkn2  27822  clwwlkwwlksb  27833  eclclwwlkn1  27854  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknonel  27874  clwwlknon1  27876  clwwlknun  27891  1pthon2v  27932  uhgr3cyclex  27961  isconngr  27968  isconngr1  27969  eupthres  27994  eupth2lems  28017  frgr0v  28041  frgr3vlem2  28053  fusgr2wsp2nb  28113  extwwlkfab  28131  numclwwlk1lem2foa  28133  numclwwlk1lem2fo  28137  isvclem  28354  isnvlem  28387  isphg  28594  isph  28599  phoeqi  28634  ubthlem3  28649  minvecolem5  28658  minvecolem6  28659  minvecolem7  28660  hhph  28955  issh3  28996  nmopub  29685  nmfnleub  29702  adjeq  29712  adjvalval  29714  elunop2  29790  lnophm  29796  nmcexi  29803  cnlnadjlem5  29848  cnlnadjeui  29854  adjbd1o  29862  jpi  30047  mddmd2  30086  chrelati  30141  chrelat2i  30142  cvexchlem  30145  dmdbr5ati  30199  cdjreui  30209  cdj3i  30218  elunsn  30273  disjunsn  30344  opeldifid  30349  fcoinvbr  30358  brabgaf  30359  opabdm  30362  opabrn  30363  iunsnima  30369  nfpconfp  30377  elimampt  30383  abfmpunirn  30397  fmptcof2  30402  funcnvmpt  30412  funcnv5mpt  30413  brsnop  30429  brprop  30433  f1od2  30457  resf1o  30466  fpwrelmap  30469  iocinioc2  30502  eliccioo  30607  wrdt2ind  30627  posrasymb  30644  isslmd  30830  fedgmullem2  31026  smatrcl  31061  pstmxmet  31137  prsdm  31157  prsrn  31158  ordtconnlem1  31167  xrmulc1cn  31173  ispisys2  31412  elcarsg  31563  eulerpartlemmf  31633  isrrvv  31701  reprinrn  31889  tgoldbachgt  31934  bnj976  32049  bnj944  32210  bnj1173  32274  bnj1321  32299  bnj1373  32302  bnj1417  32313  lfuhgr  32364  revwlk  32371  usgrgt2cycl  32377  subfacp1lem3  32429  subfacp1lem6  32432  subfacp1  32433  txpconn  32479  sconnpi1  32486  resconn  32493  cvmscbv  32505  cvmsval  32513  cvmlift2lem13  32562  cvmlift3lem2  32567  cvmlift3  32575  goeleq12bg  32596  satfvsucsuc  32612  satfbrsuc  32613  fmlafvel  32632  satffunlem2lem1  32651  satefvfmla1  32672  mclsrcl  32808  br8  32992  br6  32993  br4  32994  elintfv  33007  fv1stcnv  33020  fv2ndcnv  33021  distel  33048  frpomin  33078  poseq  33095  wsuclem  33112  sltsolem1  33180  nosupdm  33204  nosupbnd1lem4  33211  slenlt  33231  sleloe  33233  etasslt  33274  madeval2  33290  imageval  33391  funpartfv  33406  dfrdg4  33412  altopthg  33428  altopthbg  33429  brcolinear2  33519  lineext  33537  brsegle  33569  seglelin  33577  broutsideof2  33583  isfne4  33688  isfne2  33690  isfne3  33691  fneval  33700  topfneec  33703  neibastop2lem  33708  neibastop2  33709  neifg  33719  filnetlem4  33729  onsuct0  33789  bj-19.41t  34103  bj-tagcg  34300  bj-projval  34311  bj-restuni  34391  opelopabd  34436  opelopabb  34437  brabd0  34442  bj-opelid  34451  bj-ideqg  34452  bj-opelidres  34456  bj-ideqg1  34459  bj-elid6  34465  bj-isvec  34572  bj-isclm  34575  bj-isrvecd  34582  csbwrecsg  34611  csboprabg  34614  csbmpo123  34615  topdifinffinlem  34631  isbasisrelowllem1  34639  isbasisrelowllem2  34640  rdgeqoa  34654  csbfinxpg  34672  nlpineqsn  34692  wl-had1  34758  wl-had0bi  34759  wl-sbrimt  34801  wl-sblimt  34802  wl-sbnf1  34806  wl-mo2df  34821  wl-eudf  34823  wl-mo2t  34826  wl-mo3t  34827  wl-ax11-lem6  34837  wl-dfclab  34843  uncov  34888  tan2h  34899  matunitlindf  34905  ptrest  34906  poimirlem2  34909  poimirlem16  34923  poimirlem19  34926  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  cnambfre  34955  itg2addnclem2  34959  fdc  35035  heibor1  35103  rrncmslem  35125  rrnheibor  35130  opidonOLD  35145  issmgrpOLD  35156  ismndo  35165  isrngo  35190  isdivrngo  35243  isfldidl2  35362  isdmn3  35367  releleccnv  35533  releccnveq  35534  brcnvep  35541  elecres  35549  eleccnvep  35553  ideq2  35580  extid  35583  relcnveq3  35593  eqres  35612  brrabga  35613  ecin0  35621  alrmomodm  35628  brxrn  35641  brxrn2  35642  elecxrn  35653  br1cnvxrn2  35659  elec1cnvxrn2  35660  br1cossinres  35702  br1cossxrnres  35703  eldmcoss  35713  elrels2  35741  elrelscnveq3  35746  br1cnvssrres  35760  brcnvssr  35761  dfrefrels2  35768  dfcnvrefrels2  35781  dfsymrels2  35796  elrefsymrelsrel  35822  dftrrels2  35826  erim2  35926  eldisjs5  35974  prtlem13  36019  prter3  36033  lrelat  36165  islshpat  36168  lshpsmreu  36260  lkrpssN  36314  cmtvalN  36362  omllaw2N  36395  cvrval  36420  cvrval2  36425  cvlsupr3  36495  3dim0  36608  islln2  36662  islpln5  36686  islpln2  36687  islpln2ah  36700  islvol5  36730  islvol2  36731  4atlem11  36760  pmapglbx  36920  cdleme18d  37446  cdlemefrs29bpre0  37547  cdlemb3  37757  cdlemg33b  37858  cdlemkid3N  38084  cdlemkid4  38085  dvhb1dimN  38137  dia11N  38199  cdlemm10N  38269  dib11N  38311  dib1dim  38316  dibglbN  38317  diblsmopel  38322  dihopelvalcpre  38399  dih11  38416  dihmeetlem4preN  38457  dihmeetlem13N  38470  lcfrvalsnN  38692  lcfrlem9  38701  lcf1o  38702  mapdval4N  38783  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  hdmap1fval  38947  hdmapfval  38978  hdmapglem7a  39078  hlhillcs  39109  frlmfielbas  39159  addsubeq4com  39186  prjspreln0  39279  ellz1  39384  lzunuz  39385  fz1eqin  39386  diophrex  39392  rexrabdioph  39411  rexfrabdioph  39412  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  fzneg  39599  expdioph  39640  wepwsolem  39662  fnwe2lem2  39671  islmodfg  39689  kercvrlsm  39703  cnvcnvintabd  39980  iunrelexpuztr  40084  brtrclfv2  40092  frege124d  40126  rcompleq  40390  or3or  40391  uneqsn  40393  clsk1independent  40416  ntrclsneine0lem  40434  ntrclsiso  40437  ntrclsk2  40438  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  ntrclsk4  40442  ntrneiel2  40456  ntrneiiso  40461  ntrneikb  40464  ntrneik3  40466  ntrneix3  40467  ntrneik13  40468  ntrneix13  40469  ntrneik4w  40470  k0004lem3  40519  scottabf  40596  pm10.52  40717  iotasbc  40771  pm14.122a  40774  pm14.122b  40775  pm14.123a  40777  rusbcALT  40791  fvsb  40804  trsbc  40894  wessf1ornlem  41465  imassmpt  41557  limcperiod  41929  limsupre  41942  dvbdfbdioo  42235  stoweidlem34  42339  fourierdlem108  42519  fourierdlem110  42521  etransc  42588  funressnfv  43298  dfafn5a  43379  ndfatafv2nrn  43440  afv2ndefb  43443  dfatsnafv2  43471  dfatdmfcoafv2  43473  dfatco  43475  afv2fv0xorb  43486  readdcnnred  43523  resubcnnred  43524  recnmulnred  43525  cndivrenred  43526  elfz2z  43535  el1fzopredsuc  43545  elsetpreimafvb  43564  iccelpart  43613  ichal  43647  reupr  43704  lighneallem2  43791  dfeven2  43834  gbowge7  43948  sbgoldbwt  43962  isupwlk  44031  uspgrsprfo  44043  ismhm0  44092  inclfusubc  44158  isrnghm  44183  rnghmval2  44186  uzlidlring  44220  lidldomnnring  44221  zrninitoringc  44362  opeliun2xp  44401  snlindsntor  44546  elbigo2  44632  resum2sqorgt0  44716  rrx2pnedifcoorneor  44723  rrx2plord  44727  rrx2plordisom  44730  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  rrx2linest2  44751  itsclc0b  44779  itsclinecirc0in  44782  inlinecirc02plem  44793  gte-lte  44843  gt-lt  44844