Theorem syl5bb 265

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
syl5bb.1	|- ( ph <-> ps )
syl5bb.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5bb	|- ( ch -> ( ph <-> th ) )

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3		syl5bb.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrd 261	1 |- ( ch -> ( ph <-> th ) )

Syntax hints:   -> wi 4   <-> wb 189

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 190

This theorem is referenced by:  syl5rbb  266  syl5bbr  267  3bitr4g  296  imim21b  373  ifpfal  1447  cad0  1530  ax12wdemo  1919  sbal2  2300  necon3abid  2671  necon3bid  2679  r19.21tOLD  2797  ceqsralt  3082  ralxpxfr2d  3175  ceqsrexv  3183  ceqsrex2v  3185  elab2g  3198  elrabf  3205  elrab3t  3206  eueq2  3223  eqreu  3241  reu8  3245  ru  3277  sbcralt  3351  sbcabel  3356  sbcel1g  3787  sbcel2  3789  csbnestgf  3796  sbccsb2  3805  disjpss  3826  sbcssg  3891  rexsng  4018  ralprg  4032  rexprg  4033  difsn  4118  preq2b  4159  opthpr  4165  preqsnd  4171  ralunsn  4199  csbuni  4239  dfiin2g  4324  iunxsng  4373  elpwuni  4382  disjxun  4413  sbcbr12g  4469  pwnss  4581  opthneg  4694  otthg  4698  opelopabt  4726  opelopabga  4727  brabga  4728  csbmpt12  4748  rbropapd  4753  dfid3  4768  frirr  4829  wereu2  4849  brab2a  4902  opeliunxp  4904  posn  4921  sosn  4922  frsn  4923  brab2ga  4928  opbrop  4932  csbcnvgALT  5037  elrnmpt1  5101  elrnmptg  5102  eliniseg2  5227  poleloe  5249  xpdifid  5283  cnvpo  5392  elpred  5411  ordtri4  5478  oneqmini  5492  elsucg  5508  elsuc2g  5509  sbcfung  5623  dffun8  5627  fncnv  5668  fununi  5670  fnssresb  5709  fnimaeq0  5718  funcocnv2  5860  csbfv12  5922  dffn5  5932  funimass4  5938  fnsnfv  5947  dmfco  5961  fndmdif  6008  fvimacnvi  6018  fvimacnvALT  6023  unpreima  6028  respreima  6031  fmptco  6079  fressnfv  6101  fmptsnd  6109  fnnfpeq0  6118  tpres  6140  elunirn  6180  dff13  6183  f12dfv  6196  f13dfv  6197  fliftel  6226  isoini  6253  f1oiso  6266  eloprabga  6409  resoprab2  6419  elrnmpt2res  6436  ralrnmpt2  6437  ovid  6439  ov  6442  ovg  6461  ofrfval2  6575  dfwe2  6634  ssonprc  6645  ordpwsuc  6668  dfom2  6720  f1oweALT  6803  el2xptp0  6863  fmpt2x  6885  ovmptss  6903  1stconst  6910  2ndconst  6911  fnsuppres  6968  brtpos2  7004  mpt2curryd  7041  dfsmo2  7091  rdglim2  7175  seqomlem2  7193  omeu  7311  oeeui  7328  brdifun  7415  eqerlem  7420  brecop  7481  erovlem  7484  eceqoveq  7493  mapsn  7538  ixpsnval  7550  mptelixpg  7584  map1  7673  xpsnen  7681  xpdom2  7692  omxpenlem  7698  xpf1o  7759  mapunen  7766  onfin  7788  fimaxg  7843  fodomfib  7876  fofinf1o  7877  fipreima  7905  supub  7998  infglb  8031  infglbb  8032  fiming  8039  fiinfg  8040  ordtypecbv  8057  ordtypelem3  8060  ordtypelem9  8066  hartogslem1  8082  wofib  8085  wemapsolem  8090  wemapso2lem  8092  noinfep  8190  cantnf  8223  rankbnd2  8365  domtri2  8448  infxpenc2  8478  fseqdom  8482  acni2  8502  dfac9  8591  cfeq0  8711  cfsuc  8712  cflim3  8717  cfslb  8721  cofsmo  8724  enfin2i  8776  isfin3ds  8784  isf33lem  8821  fin1a2lem5  8859  axdc2lem  8903  zorn2g  8958  fodomb  8979  brdom7disj  8984  brdom6disj  8985  iundom2g  8990  cfpwsdom  9034  elgch  9072  fpwwe2cbv  9080  fpwwecbv  9094  pwfseqlem3  9110  pwfseqlem4a  9111  pwfseqlem4  9112  ltpiord  9337  nlt1pi  9356  nqereu  9379  addclprlem1  9466  1idpr  9479  reclem3pr  9499  ltsosr  9543  map2psrpr  9559  supsrlem  9560  axrrecex  9612  xrlenlt  9724  eqlei2  9770  addsubeq4  9915  renegcli  9960  lesub0  10158  wloglei  10173  conjmul  10351  rereccl  10352  infm3  10595  supaddc  10601  supadd  10602  supmul1  10603  supmullem1  10604  supmullem2  10605  supmul  10606  creui  10631  nndiv  10677  elznn0  10980  prime  11044  eqreznegel  11277  zsupss  11281  rebtwnz  11291  negelrp  11361  ltxr  11443  elixx3g  11676  ixxun  11679  ioo0  11689  ico0  11710  ioc0  11711  icc0  11712  difreicc  11792  divelunit  11802  iccf1o  11804  elfz2  11819  fzn  11843  fznn  11891  fzshftral  11910  nelfzo  11955  fzosplitsni  12049  om2uzisoi  12199  rabssnn0fi  12229  mptnn0fsupp  12240  sq11i  12396  hashsdom  12591  fi1uzind  12682  wrdval  12706  csbwrdg  12731  wrd2ind  12870  s2f1o  13046  cjreb  13234  rexfiuz  13458  cau3lem  13465  rlim2  13608  ello12  13628  ello1mpt  13633  elo12  13639  o1lo1  13649  lo1resb  13676  o1resb  13678  o1compt  13699  caucvgb  13794  mertens  13990  ruclem12  14341  divides  14355  odd2np1  14413  oddm1even  14414  sadadd2lem2  14472  gcdcllem2  14522  bezoutlem2OLD  14552  bezoutlem3OLD  14553  bezoutlem4OLD  14554  bezoutlem2  14555  bezoutlem3  14556  bezoutlem4  14557  isprm2  14680  isprm3  14681  prmreclem2  14909  prmreclem5  14912  prmreclem6  14913  4sqlem2  14941  4sqlem12  14948  vdwmc  14976  vdwpc  14978  vdwlem6  14984  vdwlem10  14988  vdwnn  14996  ramval  15008  ramvalOLD  15009  0ram  15026  prdsleval  15423  pwsle  15438  imasleval  15495  xpsfrnel2  15519  xpsle  15535  isacs2  15607  mreacs  15612  acsfn  15613  iscatd2  15635  catpropd  15662  ciclcl  15755  cicrcl  15756  isssc  15773  evlfcl  16155  uncfcurf  16172  pltval  16254  lublecllem  16282  tosso  16330  oduleg  16426  oduclatb  16438  posglbmo  16441  isipodrs  16455  odudlatb  16490  gsumvalx  16561  sgrp2rid2  16708  grplmulf1o  16776  grplactcnv  16802  elnmz  16904  eqgid  16917  isghm  16931  ghmeqker  16957  resscntz  17033  symg1bas  17085  pgrpsubgsymgbi  17096  symgfixelq  17122  f1omvdconj  17135  odmulgeq  17256  sylow3lem3  17329  sylow3lem6  17332  efgval2  17422  efgsdm  17428  efgrelexlema  17447  efgcpbllemb  17453  iscyggen2  17564  cyggenod  17567  gsummptfzcl  17649  eldprd  17684  dprdf11  17704  dprddisj2  17720  pgpfac1lem2  17756  pgpfac1  17761  srg1zr  17810  drngid2  18039  issubrg  18056  islmod  18143  aspval2  18619  psrbag  18636  cply1coe0bi  18942  zndvds  19168  znleval  19173  iunocv  19292  pjfval2  19320  pjdm2  19322  dsmmelbas  19350  ellspd  19408  islindf  19418  islindf4  19444  istopg  19973  basgen2  20053  isclo  20151  mretopd  20156  isnei  20167  isperf3  20217  restdis  20242  neitr  20244  restcls  20245  restlp  20247  restperf  20248  iscn  20299  iscnp  20301  lmbr2  20323  lmbrf  20324  ordtt1  20443  cmpsub  20463  hauscmplem  20469  cmpfi  20471  dfcon2  20482  1stcelcls  20524  1stccn  20526  nllyi  20538  subislly  20544  dissnlocfin  20592  elkgen  20599  ptpjpre1  20634  ptuni2  20639  ptclsg  20678  ptcnplem  20684  txcn  20689  hausdiag  20708  txhaus  20710  txkgen  20715  xkoptsub  20717  cnmpt21  20734  elqtop  20760  tgqtop  20775  r0cld  20801  elfg  20934  fbasrn  20947  trfil2  20950  trfil3  20951  fin1aufil  20995  elfm2  21011  elfm3  21013  flimopn  21038  fbflim  21039  flfnei  21054  flftg  21059  cnpflf2  21063  txflf  21069  fclsbas  21084  alexsubALTlem4  21113  cnextfvval  21128  snclseqg  21178  tgphaus  21179  tsmsfbas  21190  tsmssubm  21205  utopsnneip  21311  prdsxmetlem  21431  imasdsf1olem  21436  xpsdsval  21444  blres  21494  isxms2  21511  metcnp  21604  txmetcnp  21610  txmetcn  21611  metustel  21613  metuel2  21628  dscopn  21636  isngp4  21673  cnblcld  21843  metnrmlem1a  21923  metnrmlem1aOLD  21938  icoopnst  22015  iocopnst  22016  elpi1  22124  lmmbr2  22277  cfil3i  22287  caucfil  22301  iscmet3  22311  lmclim  22320  metcld2  22324  bcthlem4  22343  minveclem3b  22418  minveclem6  22424  minveclem7  22425  minveclem3bOLD  22430  minveclem6OLD  22436  minveclem7OLD  22437  ivthle  22455  ivthle2  22456  evthicc2  22459  ovolfioo  22468  ovolficc  22469  ovolgelb  22481  dyadmax  22604  subopnmbl  22610  ismbf3d  22658  mbfimaopnlem  22659  mbfimaopn2  22661  mbfaddlem  22664  mbfsup  22668  mbfinf  22669  mbfinfOLD  22670  i1f1lem  22695  i1fmulclem  22708  itg1climres  22720  mbfi1fseqlem4  22724  itg2monolem1  22756  itg2gt0  22766  isibl  22771  iblcnlem1  22793  ellimc2  22880  dvcnvrelem1  23017  itgsubst  23049  mdegleb  23061  fta1glem2  23165  quotval  23293  vieta1lem1  23311  vieta1lem2  23312  ulm2  23388  ulmcaulem  23397  ulmcau  23398  radcnvlt1  23421  sineq0  23524  cos11  23530  recosf1o  23532  efopn  23651  cxpeq  23745  mcubic  23821  birthdaylem3  23927  rlimcnp  23939  xrlimcnp  23942  eldmgm  23995  dmgmaddn0  23996  lgamgulmlem6  24007  wilth  24044  isppw  24089  isppw2  24090  mumullem2  24155  sqff1o  24157  dvdsmulf1o  24171  fsumvma  24189  fsumvma2  24190  vmasum  24192  chpchtsum  24195  lgsne0  24309  lgseisenlem2  24326  lgsquadlem1  24330  lgsquadlem2  24331  dchrmusumlema  24379  rpvmasum2  24398  dchrisum0lema  24400  pntibndlem3  24478  pntlemi  24490  pntleml  24497  pnt3  24498  trgcgrg  24608  tgcgr4  24624  colcom  24651  colrot1  24652  ltgov  24690  hlcomb  24696  lncom  24715  mirreu3  24747  isperp  24805  perpcom  24806  brbtwn  24977  brcgr  24978  brbtwn2  24983  colinearalg  24988  axeuclidlem  25040  axcontlem2  25043  axcontlem4  25045  axcontlem7  25048  nbgraf1olem1  25217  nbgraf1olem5  25221  nbcusgra  25239  uvtx01vtx  25268  cusgrauvtxb  25272  iswlk  25296  istrl  25315  ispth  25346  isspth  25347  wlkdvspthlem  25385  usgrcyclnl2  25417  wwlkn0s  25481  wwlkextwrd  25504  wwlkextproplem3  25519  isclwlk0  25530  clwwlkn2  25551  eclclwwlkn1  25608  eleclclwwlkn  25609  hashecclwwlkn1  25610  usghashecclwwlk  25611  clwlkfclwwlk1hashn  25617  clwlkfoclwwlk  25621  usg2spthonot  25664  isrgra  25702  isrusgra  25703  isrusgusrg  25708  eupath2  25756  frgra3vlem2  25777  frgrancvvdeqlem2  25807  frgrancvvdeqlem3  25808  frgrancvvdeqlemC  25815  usg2spot2nb  25841  grpodiveq  26032  opidonOLD  26098  issmgrpOLD  26110  ismndo  26119  isrngo  26154  isdivrngo  26207  isvclem  26244  isnvlem  26277  isphg  26506  isph  26511  phoeqi  26547  ubthlem3  26562  minvecolem5  26571  minvecolem6  26572  minvecolem7  26573  minvecolem5OLD  26581  minvecolem6OLD  26582  minvecolem7OLD  26583  hhph  26879  issh3  26920  nmopub  27609  nmfnleub  27626  adjeq  27636  adjvalval  27638  elunop2  27714  lnophm  27720  nmcexi  27727  cnlnadjlem5  27772  cnlnadjeui  27778  adjbd1o  27786  jpi  27971  mddmd2  28010  chrelati  28065  chrelat2i  28066  cvexchlem  28069  dmdbr5ati  28123  cdjreui  28133  cdj3i  28142  iunxsngf  28220  disjunsn  28252  opeldifid  28258  fcoinvbr  28263  brabgaf  28264  opabdm  28267  opabrn  28268  iunsnima  28272  abfmpunirn  28299  feqmptdf  28306  fmptcof2  28307  funcnvmptOLD  28318  funcnvmpt  28319  funcnv5mpt  28320  f1od2  28357  resf1o  28363  fpwrelmap  28366  iocinioc2  28409  eliccioo  28448  posrasymb  28466  isslmd  28566  smatrcl  28670  pstmxmet  28748  prsdm  28768  prsrn  28769  ordtconlem1  28778  xrmulc1cn  28784  ispisys2  29023  elcarsg  29185  eulerpartlemmf  29256  isrrvv  29324  bnj976  29637  bnj944  29797  bnj1173  29859  bnj1321  29884  bnj1373  29887  bnj1417  29898  subfacp1lem3  29953  subfacp1lem6  29956  subfacp1  29957  txpcon  30003  sconpi1  30010  rescon  30017  cvmscbv  30029  cvmsval  30037  cvmlift2lem13  30086  cvmlift3lem2  30091  cvmlift3  30099  mclsrcl  30247  br8  30444  br6  30445  br4  30446  fv1stcnv  30470  fv2ndcnv  30471  distel  30498  poseq  30539  wsuclem  30556  sltsolem1  30605  imageval  30745  funpartfv  30760  dfrdg4  30766  altopthg  30782  altopthbg  30783  brcolinear2  30873  lineext  30891  brsegle  30923  seglelin  30931  broutsideof2  30937  isfne4  31044  isfne2  31046  isfne3  31047  fneval  31056  topfneec  31059  neibastop2lem  31064  neibastop2  31065  neifg  31075  filnetlem4  31085  onsuct0  31149  bj-abbi  31434  bj-tagcg  31623  bj-projval  31634  csbopg2  31769  csbwrecsg  31772  csboprabg  31775  csbmpt22g  31776  topdifinffinlem  31794  isbasisrelowllem1  31802  isbasisrelowllem2  31803  rdgeqoa  31817  csbfinxpg  31824  wl-sbrimt  31922  wl-sblimt  31923  wl-sbnf1  31927  wl-mo2df  31943  wl-eudf  31945  wl-mo2t  31948  wl-mo3t  31949  wl-ax11-lem6  31964  tan2h  31981  ptrest  31983  poimirlem2  31986  poimirlem16  32000  poimirlem19  32003  poimirlem23  32007  poimirlem24  32008  poimirlem25  32009  poimirlem26  32010  poimirlem27  32011  mbfposadd  32032  cnambfre  32033  itg2addnclem2  32038  fdc  32118  heibor1  32186  rrncmslem  32208  rrnheibor  32213  isfldidl2  32346  isdmn3  32351  prtlem13  32484  prter3  32498  lrelat  32624  islshpat  32627  lshpsmreu  32719  lkrpssN  32773  cmtvalN  32821  omllaw2N  32854  cvrval  32879  cvrval2  32884  cvlsupr3  32954  3dim0  33066  islln2  33120  islpln5  33144  islpln2  33145  islpln2ah  33158  islvol5  33188  islvol2  33189  4atlem11  33218  pmapglbx  33378  cdleme18d  33905  cdlemefrs29bpre0  34007  cdlemb3  34217  cdlemg33b  34318  cdlemkid3N  34544  cdlemkid4  34545  dvhb1dimN  34597  dia11N  34660  cdlemm10N  34730  dib11N  34772  dib1dim  34777  dibglbN  34778  diblsmopel  34783  dihopelvalcpre  34860  dih11  34877  dihmeetlem4preN  34918  dihmeetlem13N  34931  lcfrvalsnN  35153  lcfrlem9  35162  lcf1o  35163  mapdval4N  35244  baerlem3lem2  35322  baerlem5alem2  35323  baerlem5blem2  35324  hdmap1fval  35409  hdmapfval  35442  hdmapglem7a  35542  hlhillcs  35573  ellz1  35653  lzunuz  35654  fz1eqin  35655  diophrex  35662  rexrabdioph  35681  rexfrabdioph  35682  2rexfrabdioph  35683  3rexfrabdioph  35684  4rexfrabdioph  35685  6rexfrabdioph  35686  7rexfrabdioph  35687  fzneg  35876  expdioph  35922  wepwsolem  35944  fnwe2lem2  35953  islmodfg  35971  kercvrlsm  35985  sdrgacs  36111  cnvcnvintabd  36250  iunrelexpuztr  36355  brtrclfv2  36363  frege124d  36397  pm10.52  36757  iotasbc  36813  pm14.122a  36816  pm14.122b  36817  pm14.123a  36819  rusbcALT  36833  fvsb  36848  trsbc  36944  rexsngf  37428  iunxsngf2  37439  mapsnd  37513  limcperiod  37745  limsupre  37758  limsupreOLD  37759  dvbdfbdioo  37839  stoweidlem34  37932  fourierdlem108  38115  fourierdlem110  38117  etransc  38186  2reu4a  38647  funressnfv  38666  dfafn5a  38699  el1fzopredsuc  38759  iccelpart  38784  dfeven2  38816  gboge7  38901  bgoldbwt  38915  riotaeqimp  39078  elfz2z  39096  isuhgr  39196  isushgr  39197  isupgr  39222  isumgr  39231  isuspgr  39286  isusgr  39287  uhgr0v0e  39363  isfusgrf1  39436  opfusgr  39438  usgr1v0e  39441  nbuhgr2vtx1edgb  39469  edgnbusgreu  39490  nbusgredgeu0  39491  isuvtxa  39516  cusgruvtxb  39539  cplgr3v  39551  cusgrsizeinds  39562  vtxdg0v  39582  uhgrvd0nedgb  39594  vtxduhgr0nedg  39595  vtxdusgr0edgnelALT  39599  is1wlk  39675  isWlk  39676  1wlk1walk  39696  upgr2wlk  39714  isclWlke  39803  1pthon2v-av  39867  umgr2wlk  39897  uhgr3cyclex  39922  isconngr  39929  isconngr1  39930  usgra2pthlem1  39939  isuhgrALTV  39950  isushgrALTV  39951  usgo0s0ALT  40020  usgo1s0ALT  40021  ismhm0  40077  inclfusubc  40139  isrnghm  40164  rnghmval2  40167  uzlidlring  40201  lidldomnnring  40202  zrninitoringc  40345  opeliun2xp  40386  snlindsntor  40536  elbigo2  40635  gte-lte  40716  gt-lt  40717