Theorem sylib 122

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.)

Hypotheses

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

Assertion

Ref	Expression
sylib	⊢ (𝜑 → 𝜒)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylib.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	biimpi 120	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb1  137  bicomd  141  pm5.74d  182  bitri  184  3imtr3i  200  ancomd  267  pm4.71d  397  pm4.71rd  398  imdistand  451  orcomd  741  3mix3  1199  mpjao3dan  1348  ecase23d  1391  exlimdh  1649  nexd  1666  alexnim  1701  excomim  1715  19.41  1738  equcomd  1759  nfexd  1814  sbh  1829  sbcof2  1863  sbidm  1904  sb6rf  1906  nfsbt  2036  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eu2  2131  2euex  2174  eqcomd  2244  3eltr3g  2323  abbid  2355  neneqd  2441  eqnetrrid  2451  3netr3g  2454  necomd  2506  r19.21bi  2638  nrexdv  2643  rexlimd  2665  rabbidva  2809  elisset  2836  euind  3013  rmoan  3026  reuind  3031  2rmorex  3032  spsbc  3063  spesbc  3138  eldifad  3231  eldifbd  3232  3sstr3g  3290  sseqtrdi  3296  difindiss  3485  un00  3567  vvin  3569  undifss  3608  ifcldcd  3678  disjpr2  3773  difprsn1  3854  diftpsn3  3856  difsnss  3861  sneqr  3885  preqr1  3893  preq12b  3895  oprcl  3928  intab  3999  riinm  4085  rintm  4105  disjiun  4125  sndisj  4126  3brtr3g  4163  trint  4244  iinexgm  4290  exmidexmid  4333  exmid01  4335  pwntru  4336  exmid1stab  4345  pwel  4358  exss  4367  0nelop  4388  euotd  4395  opelopabsb  4402  pwunim  4431  issod  4464  frind  4497  suctr  4566  orduniss  4570  onelini  4575  oneluni  4576  eusv2i  4601  rexxfrd  4609  rabxfrd  4615  reuhypd  4617  iunpw  4626  sucexg  4645  ordsucim  4647  ordtriexmidlem  4666  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsucunielexmid  4678  orddif  4694  suc11g  4704  onintexmid  4720  reg3exmidlemwe  4726  tfisi  4734  peano1  4741  peano2  4742  finds2  4748  omsinds  4769  brrelex12  4813  brel  4827  ssrel  4863  ssrel2  4865  ssrelrel  4875  elrel  4877  xpsspw  4887  relop  4930  dmxpm  5002  opelresi  5074  mptimass  5139  ndmima  5164  poirr2  5180  xpmlem  5208  xpimasn  5236  iotass  5355  iotacl  5362  dffun5r  5389  funeu  5402  funeu2  5403  funfnd  5408  funopg  5411  funun  5422  fununfun  5424  funinsn  5430  funtp  5434  funcnvuni  5450  funcnvres2  5456  imadiflem  5460  imadif  5461  funimaexglem  5464  fneu2  5488  fnimaeq0  5505  fnmpt  5510  ffrn  5545  fun2  5562  f00  5584  f0bi  5585  fimadmfo  5624  foimacnv  5657  resdif  5661  f1ococnv1  5668  fv3  5718  relelfvdm  5727  elfvm  5729  nfvres  5732  dffn5im  5748  mptfvex  5791  fvmptdf  5793  fvmptdv2  5795  fndmdif  5814  dff4im  5854  fmpt  5858  fmptd  5862  fmptdf  5865  f1oresrab  5873  fcoconst  5879  fsn  5880  funopsn  5891  ftpg  5899  fsnunf  5915  resfunexg  5936  mptmex  5945  isores1  6020  riota2df  6060  acexmidlemcase  6080  brabvv  6134  funoprabg  6187  fnovim  6197  ovmpodf  6220  ovi3  6226  elmpocl  6284  uchoice  6371  1stcof  6397  2ndcof  6398  opabn1stprc  6429  fnmpo  6438  fmpoco  6452  fo2ndf  6463  f1o2ndf1  6464  disjxp1  6472  fvdifsuppst  6484  fsuppeq  6487  fsuppeqg  6488  suppssrst  6501  suppssrgst  6502  brtpos2  6522  reldmtpos  6524  dftpos3  6533  dftpos4  6534  tpostpos2  6536  tposf2  6539  tposf12  6540  tposfo  6542  tposf  6543  smores2  6565  tfrlem1  6579  tfrlem3-2d  6583  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcldm  6634  rdgivallem  6652  rdgisucinc  6656  frecabex  6669  frecfnom  6672  frecfcllem  6675  frecsuclem  6677  omsuc  6745  nntri2  6767  nnsucuniel  6768  nnsseleq  6774  nnm00  6803  ecexr  6812  swoer  6835  elqsn0m  6877  iinerm  6881  erinxp  6883  ecinxp  6884  eroveu  6900  eroprf  6902  mapprc  6926  mapsn  6972  ixpprc  7001  ixp0  7013  resixp  7015  elixpsn  7017  dom2lem  7058  fundmen  7094  1dom1el  7107  dom0  7138  xpf1o  7144  mapxpen  7148  xpmapenlem  7149  ssenen  7152  nneneq  7158  ssfilem  7177  ssfilemd  7179  dif1en  7183  dif1enen  7184  fin0  7189  fin0or  7190  diffitest  7191  diffisn  7197  ac6sfi  7202  fimax2gtrilemstep  7205  fimax2gtri  7206  finexdc  7207  eqsndc  7210  exmidpweq  7216  pw1fin  7217  onunsnss  7224  unsnfidcel  7228  undifdcss  7230  undifdc  7231  tpfidceq  7237  fiintim  7238  fisseneq  7242  fidcenumlemr  7272  sbthlemi4  7277  sbthlemi5  7278  sbthlemi9  7282  fifo  7314  2omap  7318  suplubti  7340  supelti  7342  infmoti  7368  infisoti  7372  djulclb  7395  updjud  7422  omp1eomlem  7434  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumct  7455  nninfninc  7463  nnnninfeq2  7469  finomni  7480  fodjuomnilemdc  7484  fodjum  7486  fodjuomnilemres  7488  fodjumkvlemres  7499  omniwomnimkv  7507  nninfwlporlem  7513  nninfwlpoimlemginf  7516  nninfwlpoim  7519  nninfinfwlpo  7520  ficardon  7534  pr2cv1  7541  exmidonfinlem  7545  en2eleq  7547  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemim  7553  finacn  7560  acfun  7563  exmidaclem  7564  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  pw1if  7584  pw1on  7585  papsym  7612  papcotr  7613  dftap2  7617  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  cc1  7631  cc2lem  7632  cc2  7633  cc3  7634  acnccim  7638  elni2  7681  indpi  7709  distrnqg  7754  subhalfnqq  7781  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nnnq0lem1  7813  distrnq0  7826  elinp  7841  elnp1st2nd  7843  prltlu  7854  prnmaxl  7855  prnminu  7856  prarloc  7870  nqprm  7909  appdivnq  7930  prmuloc  7933  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemlol  8065  caucvgprprlemexbt  8073  caucvgprprlem1  8076  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  gt0srpr  8115  caucvgsrlemcl  8156  caucvgsrlembound  8161  caucvgsrlemgt1  8162  suplocsrlemb  8173  suplocsrlem  8175  suplocsr  8176  ltresr  8206  nnindnn  8260  axcaucvglemcl  8262  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  sup3exmid  9288  indconst0  9303  indconst1  9304  nnind  9321  nn0supp  9621  nn0ge2m1nn  9629  zleloe  9693  zapne  9721  nn0lt2  9729  suprzclex  9746  zindd  9766  uzm1  9955  uzin  9957  infregelbex  10000  elnn1uz2  10009  nn01to3  10019  divfnzn  10023  qapne  10041  xrltnsym2  10198  xaddass  10273  xleadd1a  10277  xlt2add  10284  xlesubadd  10287  iooval2  10319  icoshftf1o  10395  fztri3or  10445  fzneuz  10510  4fvwrd4  10549  elfzo0  10595  infssuzex  10668  infssuzcldc  10670  infssfzcldc  10671  infssfzledc  10672  suprzubdc  10673  nninfdcex  10674  zsupssdc  10675  exbtwnzlemex  10686  ioom  10697  fzfig  10869  uzennn  10875  uzsinds  10883  iseqovex  10897  seq3val  10899  seqvalcd  10900  seqf  10903  seqovcd  10906  monoord2  10925  iseqf1olemjpcl  10947  iseqf1olemqpcl  10948  seq3f1olemqsum  10952  seq3f1o  10956  seqf1og  10960  seq3distr  10971  expp1  10985  expcl2lemap  10990  expclzap  11003  expap0i  11010  nn0ltexp2  11149  bcval5  11203  hashinfuni  11218  hashennnuni  11220  hashnncl  11236  resunimafz0  11276  hashf1lem2  11288  hashf1  11289  zfz1isolemiso  11293  zfz1isolem1  11294  zfz1iso  11295  wrdsymb0  11339  wrdlen1  11344  ccat1st1st  11411  swrdrlen  11435  pfxid  11460  pfxwrdsymbg  11464  pfxtrcfv  11467  pfxccat1  11476  pfxpfxid  11483  pfxcctswrd  11484  swrdccatin1  11499  pfxccatin12  11507  pfxccatid  11515  seq3shft  11605  cvg1nlemcau  11752  rexanuz  11756  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemsqa  11792  resqrexlemex  11793  rersqreu  11796  caubnd2  11885  maxleast  11981  fimaxre2  11995  minmax  11998  xrmaxiflemcl  12013  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxadd  12029  xrminmax  12033  xrbdtri  12044  climreu  12065  reccn2ap  12081  iserex  12107  climcvg1nlem  12117  serf0  12120  fz1f1o  12143  summodclem3  12149  zsumdc  12153  fsum3  12156  isumz  12158  isumss  12160  isumss2  12162  fsumsersdc  12164  fsum3ser  12166  fsumsplit  12176  isumclim2  12191  isumclim3  12192  fsum2dlemstep  12203  fsumcnv  12206  fisumcom2  12207  bcxmas  12258  isumle  12264  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratz  12301  mertenslemub  12303  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  zproddc  12348  prod1dc  12355  fprodsplitdc  12365  fprodsplit  12366  fprodunsn  12373  fprodcl2lem  12374  fprodcllemf  12382  fprod2dlemstep  12391  fprodcnv  12394  fprodcom2fi  12395  fprodle  12409  ef0lem  12429  fsumdvds  12611  mod2eq1n2dvds  12648  ndvdssub  12699  bitsfzolem  12723  bitsfzo  12724  bitsinv1  12731  gcdsupex  12736  gcdsupcl  12737  bezoutlemnewy  12775  bezoutlemmain  12777  bezoutlembi  12784  bezoutlemeu  12786  bezoutlemle  12787  uzwodc  12816  nnwofdc  12817  nnwosdc  12818  nninfctlemfo  12819  nninfct  12820  nn0seqcvgd  12821  eucalgf  12835  eucalginv  12836  lcmval  12843  prmind2  12900  dfphi2  13000  phiprmpw  13002  phimullem  13005  eulerthlem1  13007  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemh  13011  eulerthlemth  13012  eulerth  13013  phisum  13021  odzcllem  13023  odzdvds  13026  pythagtriplem19  13063  pclemub  13068  pcprecl  13070  pceu  13076  pcqmul  13084  pcqcl  13087  pcxnn0cl  13091  pcxqcl  13093  pcge0  13094  pcdvdsb  13101  pceq0  13103  pcneg  13106  pcdvdstr  13108  pcgcd1  13109  pc2dvds  13111  pcz  13113  pcprmpw2  13114  pcaddlem  13120  pcadd  13121  pcmptcl  13123  pcmpt  13124  pcmptdvds  13126  fldivp1  13129  qexpz  13133  pockthlem  13137  pockthg  13138  prmunb  13143  1arith  13148  4sqlemffi  13177  4sqlem17  13188  4sqlem18  13189  4sqlem19  13190  ballotfilemcdc  13225  ballotfilem2  13230  ballotfilemfp1  13233  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemfmpn  13236  ballotfilemefi  13239  ballotfilemiex  13246  ballotfilemro  13268  ennnfonelemom  13301  ennnfoneleminc  13304  ennnfonelemhf1o  13306  ennnfonelemex  13307  ennnfonelemhom  13308  ennnfonelemdm  13313  ennnfonelemr  13316  ennnfonelemim  13317  exmidunben  13319  ctinfom  13321  inffinp1  13322  ctinf  13323  enctlem  13325  ctiunctlemu1st  13327  ctiunctlemu2nd  13328  ctiunctlemudc  13330  ctiunct  13333  ctiunctal  13334  unct  13335  ssomct  13338  nninfdclemcl  13341  nninfdclemp1  13343  nninfdc  13346  structcnvcnv  13370  setscom  13394  relelbasov  13418  ressbas2d  13424  ressval3d  13428  ressabsg  13432  restid2  13604  imasaddfnlemg  13637  quslem  13647  ercpbl  13654  fnpr2ob  13663  mgmplusf  13688  grpinvalem  13707  grpinva  13708  grprida  13709  fngzsum  13710  gzsumvalx  13711  gzsum0  13715  gzsumval2  13716  ismnd  13734  mhmpropd  13775  grppropd  13824  grpsubf  13886  dfgrp3mlem  13905  mulgnn0p1  13938  mulgnn0subcl  13940  mulgsubcl  13941  mulgneg  13945  mulgnn0dir  13957  mulgnn0ass  13963  submmulg  13971  issubg2m  13994  issubg4m  13998  ghmmulg  14061  ghmrn  14062  gsumvalfi  14154  gzsumgsum  14157  gsumf1ofi  14162  gsummhmfi  14166  gsumressfi  14169  lringuplu  14505  rrgsupp  14576  opprdrng  14622  lmodscaf  14649  lssintclm  14723  lspun0  14764  lidlbas  14817  psrbagconcl  15065  psr1clfi  15081  topontopon  15123  eltg3i  15159  epttop  15193  difopn  15211  uncld  15216  0nnei  15256  resttopon  15274  restabs  15278  restopnb  15284  lmcvg  15320  cnptopco  15325  cnss1  15329  cnss2  15330  cncnpi  15331  cncnp2m  15334  cnrest  15338  cnrest2  15339  cnrest2r  15340  cnptoprest  15342  cnptoprest2  15343  lmss  15349  lmff  15352  lmtopcnp  15353  lmcn  15354  txbasval  15370  upxp  15375  txcnmpt  15376  txdis1cn  15381  txlm  15382  lmcn2  15383  cnmpt11  15386  cnmpt11f  15387  cnmpt1t  15388  cnmpt12  15390  cnmpt21  15394  cnmpt21f  15395  cnmpt2t  15396  cnmpt22  15397  cnmpt22f  15398  cnmptcom  15401  hmeocnv  15410  hmeof1o  15412  hmeores  15418  txhmeo  15422  txswaphmeo  15424  isxmet2d  15451  blfvalps  15488  xblss2ps  15507  xblss2  15508  blfps  15512  blf  15513  unirnblps  15525  unirnbl  15526  isxms2  15555  bdxmet  15604  bdmet  15605  xmetxp  15610  xmettx  15613  blssioo  15656  tgioo  15657  mulcncflem  15710  divcncfap  15717  dedekindeulemuub  15720  dedekindeulemub  15721  dedekindeulemloc  15722  dedekindeulemlu  15724  suplociccreex  15727  suplociccex  15728  dedekindicclemuub  15729  dedekindicclemub  15730  dedekindicclemloc  15731  dedekindicclemlu  15733  dedekindicc  15736  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthdich  15756  limcrcl  15761  limcmpted  15766  limccnp2lem  15779  limccnp2cntop  15780  limccoap  15781  dvrecap  15816  plyaddlem1  15850  plymullem1  15851  plycoeid3  15860  plyco  15862  plycj  15864  plyrecj  15866  dvply1  15868  dvply2g  15869  cosordlem  15953  logbgcd1irraplemexp  16076  logbgcd1irrap  16078  birthdaylem2  16094  birthdaylem3  16095  lgsneg1  16156  lgsdilem  16158  lgsdir2  16164  lgsdirprm  16165  lgsdir  16166  lgsne0  16169  lgsabs1  16170  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1f1o  16191  gausslemma2dlem4  16195  lgseisenlem1  16201  lgsquadlem3  16210  2lgslem1a  16219  2sqlem5  16250  2sqlem7  16252  2sqlem8a  16253  2sqlem8  16254  2sqlem9  16255  gropeld  16302  grstructeld2dom  16303  uhgrm  16331  upgrm  16353  upgr1een  16377  uhgredgm  16389  edgupgren  16394  edgumgren  16395  edgusgren  16416  ausgrusgrben  16421  umgr2edg1  16462  usgredg2vlem1  16475  uhgr0enedgfi  16489  subupgr  16526  vtxedgfi  16542  vtxlpfi  16543  vtxdumgrfival  16551  vtxd0nedgbfi  16552  1hevtxdg0fi  16560  p1evtxdeqfilem  16564  wlkvtxm  16593  g0wlk0  16623  wlkres  16632  trlreslem  16642  clwwlkccatlem  16653  clwwlknnn  16665  trlsegvdeglem6  16718  eupth2lem3lem3fi  16723  eupth2lem3lem7fi  16727  eulerpathum  16734  dichmul0or  16772  bj-stand  16788  bj-charfundcALT  16847  bj-charfunbi  16849  bj-bdfindis  16985  bj-peano4  16993  strcollnfALT  17024  pw1map  17037  pwtrufal  17039  pwf1oexmid  17041  subctctexmid  17042  pw1nct  17045  stnot  17051  wexmiddc  17054  nnsf  17060  nninfalllem1  17063  nninfall  17064  nninfsellemqall  17070  nnnninfen  17076  exmidsbthrlem  17079  sbthom  17083  repiecef  17089  cvgcmp2nlemabs  17093  trilpo  17104  iswomni0  17113  redcwlpo  17117  dceqnconst  17122  dcapnconst  17123  nconstwlpolem  17127  nconstwlpo  17128  neapmkvlem  17129  neapmkv  17130  ltlenmkv  17132  taupi  17135  als1d  17145  als2d  17146  rals1d  17147  rals2d  17148  alseu1d  17181  alseu2d  17182  ralseu1d  17183  ralseu2d  17184  dfalseu2  17189