Theorem sylib 121

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 119	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb1  136  bicomd  140  pm5.74d  181  bitri  183  3imtr3i  199  ancomd  265  pm4.71d  391  pm4.71rd  392  imdistand  445  orcomd  724  3mix3  1163  mpjao3dan  1302  ecase23d  1345  exlimdh  1589  nexd  1606  alexnim  1641  excomim  1656  19.41  1679  equcomd  1700  nfexd  1754  sbh  1769  sbcof2  1803  sbidm  1844  sb6rf  1846  nfsbt  1969  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  eu2  2063  2euex  2106  eqcomd  2176  3eltr3g  2255  abbid  2287  neneqd  2361  eqnetrrid  2371  3netr3g  2374  necomd  2426  r19.21bi  2558  nrexdv  2563  rexlimd  2584  rabbidva  2718  elisset  2744  euind  2917  rmoan  2930  reuind  2935  2rmorex  2936  spsbc  2966  spesbc  3040  eldifad  3132  eldifbd  3133  3sstr3g  3189  sseqtrdi  3195  difindiss  3381  un00  3460  undifss  3494  ifcldcd  3560  disjpr2  3645  difprsn1  3717  diftpsn3  3719  difsnss  3724  sneqr  3745  preqr1  3753  preq12b  3755  oprcl  3787  intab  3858  riinm  3943  rintm  3963  disjiun  3982  sndisj  3983  3brtr3g  4020  trint  4100  iinexgm  4138  exmidexmid  4180  exmid01  4182  pwntru  4183  pwel  4201  exss  4210  0nelop  4231  euotd  4237  opelopabsb  4243  pwunim  4269  issod  4302  frind  4335  suctr  4404  orduniss  4408  onelini  4413  oneluni  4414  eusv2i  4438  rexxfrd  4446  rabxfrd  4452  reuhypd  4454  iunpw  4463  sucexg  4480  ordsucim  4482  ordtriexmidlem  4501  ontriexmidim  4504  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  ordsucunielexmid  4513  orddif  4529  suc11g  4539  onintexmid  4555  reg3exmidlemwe  4561  tfisi  4569  peano1  4576  peano2  4577  finds2  4583  omsinds  4604  brrelex12  4647  brel  4661  ssrel  4697  ssrel2  4699  ssrelrel  4709  elrel  4711  xpsspw  4721  relop  4759  dmxpm  4829  opelresi  4900  ndmima  4986  poirr2  5001  xpmlem  5029  xpimasn  5057  iotass  5175  iotacl  5181  dffun5r  5208  funeu  5221  funeu2  5222  funfnd  5227  funopg  5230  funun  5240  funinsn  5245  funtp  5249  funcnvuni  5265  funcnvres2  5271  imadiflem  5275  imadif  5276  funimaexglem  5279  fneu2  5301  fnimaeq0  5317  fnmpt  5322  fun2  5369  f00  5387  f0bi  5388  foimacnv  5458  resdif  5462  f1ococnv1  5469  fv3  5517  relelfvdm  5526  nfvres  5527  dffn5im  5540  mptfvex  5579  fvmptdf  5581  fvmptdv2  5583  fndmdif  5598  dff4im  5639  fmpt  5643  fmptd  5647  fmptdf  5650  f1oresrab  5658  fcoconst  5664  fsn  5665  ftpg  5677  fsnunf  5693  resfunexg  5714  isores1  5790  riota2df  5826  acexmidlemcase  5845  brabvv  5896  funoprabg  5949  fnovim  5958  ovmpodf  5981  ovi3  5986  elmpocl  6044  1stcof  6139  2ndcof  6140  fnmpo  6178  fmpoco  6192  fo2ndf  6203  f1o2ndf1  6204  disjxp1  6212  brtpos2  6227  reldmtpos  6229  dftpos3  6238  dftpos4  6239  tpostpos2  6241  tposf2  6244  tposf12  6245  tposfo  6247  tposf  6248  smores2  6270  tfrlem1  6284  tfrlem3-2d  6288  tfrlemisucaccv  6301  tfrlemibxssdm  6303  tfrlemibfn  6304  tfrlemi1  6308  tfrexlem  6310  tfr1onlemsucaccv  6317  tfr1onlembxssdm  6319  tfr1onlembfn  6320  tfr1onlemaccex  6324  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemaccex  6337  tfrcldm  6339  rdgivallem  6357  rdgisucinc  6361  frecabex  6374  frecfnom  6377  frecfcllem  6380  frecsuclem  6382  omsuc  6448  nntri2  6470  nnsucuniel  6471  nnsseleq  6477  nnm00  6505  ecexr  6514  swoer  6537  elqsn0m  6577  iinerm  6581  erinxp  6583  ecinxp  6584  eroveu  6600  eroprf  6602  mapprc  6626  mapsn  6664  ixpprc  6693  ixp0  6705  resixp  6707  elixpsn  6709  dom2lem  6746  fundmen  6780  dom0  6812  xpf1o  6818  mapxpen  6822  xpmapenlem  6823  ssenen  6825  nneneq  6831  ssfilem  6849  dif1en  6853  dif1enen  6854  fin0  6859  fin0or  6860  diffitest  6861  diffisn  6867  ac6sfi  6872  fimax2gtrilemstep  6874  fimax2gtri  6875  finexdc  6876  exmidpweq  6883  pw1fin  6884  onunsnss  6890  unsnfidcel  6894  undifdcss  6896  undifdc  6897  fiintim  6902  fisseneq  6905  fidcenumlemr  6928  sbthlemi4  6933  sbthlemi5  6934  sbthlemi9  6938  fifo  6953  suplubti  6973  supelti  6975  infmoti  7001  infisoti  7005  djulclb  7028  updjud  7055  omp1eomlem  7067  0ct  7080  ctmlemr  7081  ctssdclemn0  7083  ctssdccl  7084  ctssdc  7086  enumct  7088  nnnninfeq2  7101  finomni  7112  fodjuomnilemdc  7116  fodjum  7118  fodjuomnilemres  7120  fodjumkvlemres  7131  omniwomnimkv  7139  exmidonfinlem  7157  en2eleq  7159  exmidfodomrlemeldju  7163  exmidfodomrlemreseldju  7164  exmidfodomrlemim  7165  acfun  7171  exmidaclem  7172  exmidontriimlem3  7187  exmidontriimlem4  7188  exmidontriim  7189  pw1on  7190  ccfunen  7213  cc1  7214  cc2lem  7215  cc2  7216  cc3  7217  elni2  7263  indpi  7291  distrnqg  7336  subhalfnqq  7363  enq0sym  7381  enq0ref  7382  enq0tr  7383  nqnq0pi  7387  nnnq0lem1  7395  distrnq0  7408  elinp  7423  elnp1st2nd  7425  prltlu  7436  prnmaxl  7437  prnminu  7438  prarloc  7452  nqprm  7491  appdivnq  7512  prmuloc  7515  mullocpr  7520  distrlem4prl  7533  distrlem4pru  7534  ltexprlemm  7549  ltexprlemopl  7550  ltexprlemopu  7552  cauappcvgprlemopl  7595  cauappcvgprlemopu  7597  cauappcvgprlemdisj  7600  cauappcvgprlem2  7609  cauappcvgprlemlim  7610  caucvgprlemnkj  7615  caucvgprlemopl  7618  caucvgprlemopu  7620  caucvgprlemdisj  7623  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem2  7629  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemlol  7647  caucvgprprlemexbt  7655  caucvgprprlem1  7658  suplocexprlemrl  7666  suplocexprlemmu  7667  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemub  7672  suplocexprlemlub  7673  prsrlem1  7691  gt0srpr  7697  caucvgsrlemcl  7738  caucvgsrlembound  7743  caucvgsrlemgt1  7744  suplocsrlemb  7755  suplocsrlem  7757  suplocsr  7758  ltresr  7788  nnindnn  7842  axcaucvglemcl  7844  axcaucvglemval  7846  axcaucvglemcau  7847  axcaucvglemres  7848  axpre-suploclemres  7850  axpre-suploc  7851  sup3exmid  8860  nnind  8881  nn0supp  9174  nn0ge2m1nn  9182  zleloe  9246  zapne  9273  nn0lt2  9280  suprzclex  9297  zindd  9317  uzm1  9504  uzin  9506  infregelbex  9544  elnn1uz2  9553  nn01to3  9563  divfnzn  9567  qapne  9585  xrltnsym2  9738  xaddass  9813  xleadd1a  9817  xlt2add  9824  xlesubadd  9827  iooval2  9859  icoshftf1o  9935  fztri3or  9982  fzneuz  10044  4fvwrd4  10083  elfzo0  10125  exbtwnzlemex  10193  ioom  10204  fzfig  10373  uzennn  10379  uzsinds  10385  iseqovex  10399  seq3val  10401  seqvalcd  10402  seqf  10404  seqovcd  10406  monoord2  10420  iseqf1olemjpcl  10438  iseqf1olemqpcl  10439  seq3f1olemqsum  10443  seq3f1o  10447  seq3distr  10456  expp1  10470  expcl2lemap  10475  expclzap  10488  expap0i  10495  nn0ltexp2  10631  bcval5  10684  hashinfuni  10698  hashennnuni  10700  hashnncl  10717  resunimafz0  10753  zfz1isolemiso  10761  zfz1isolem1  10762  zfz1iso  10763  seq3shft  10789  cvg1nlemcau  10935  rexanuz  10939  resqrexlemoverl  10972  resqrexlemglsq  10973  resqrexlemsqa  10975  resqrexlemex  10976  rersqreu  10979  caubnd2  11068  maxleast  11164  fimaxre2  11177  minmax  11180  xrmaxiflemcl  11195  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxadd  11211  xrminmax  11215  xrbdtri  11226  climreu  11247  reccn2ap  11263  iserex  11289  climcvg1nlem  11299  serf0  11302  fz1f1o  11325  summodclem3  11330  zsumdc  11334  fsum3  11337  isumz  11339  isumss  11341  isumss2  11343  fsumsersdc  11345  fsum3ser  11347  fsumsplit  11357  isumclim2  11372  isumclim3  11373  fsum2dlemstep  11384  fsumcnv  11387  fisumcom2  11388  bcxmas  11439  isumle  11445  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  cvgratz  11482  mertenslemub  11484  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  zproddc  11529  prod1dc  11536  fprodsplitdc  11546  fprodsplit  11547  fprodunsn  11554  fprodcl2lem  11555  fprodcllemf  11563  fprod2dlemstep  11572  fprodcnv  11575  fprodcom2fi  11576  fprodle  11590  ef0lem  11610  mod2eq1n2dvds  11825  ndvdssub  11876  infssuzex  11891  infssuzcldc  11893  suprzubdc  11894  nninfdcex  11895  zsupssdc  11896  gcdsupex  11899  gcdsupcl  11900  bezoutlemnewy  11938  bezoutlemmain  11940  bezoutlembi  11947  bezoutlemeu  11949  bezoutlemle  11950  uzwodc  11979  nnwofdc  11980  nnwosdc  11981  nn0seqcvgd  11982  eucalgf  11996  eucalginv  11997  lcmval  12004  prmind2  12061  dfphi2  12161  phiprmpw  12163  phimullem  12166  eulerthlem1  12168  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  eulerth  12174  phisum  12181  odzcllem  12183  odzdvds  12186  pythagtriplem19  12223  pclemub  12228  pcprecl  12230  pceu  12236  pcqmul  12244  pcqcl  12247  pcxnn0cl  12251  pcge0  12253  pcdvdsb  12260  pceq0  12262  pcneg  12265  pcdvdstr  12267  pcgcd1  12268  pc2dvds  12270  pcz  12272  pcprmpw2  12273  pcaddlem  12279  pcadd  12280  pcmptcl  12281  pcmpt  12282  pcmptdvds  12284  fldivp1  12287  qexpz  12291  pockthlem  12295  pockthg  12296  prmunb  12301  1arith  12306  ennnfonelemom  12350  ennnfoneleminc  12353  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemdm  12362  ennnfonelemr  12365  ennnfonelemim  12366  exmidunben  12368  ctinfom  12370  inffinp1  12371  ctinf  12372  enctlem  12374  ctiunctlemu1st  12376  ctiunctlemu2nd  12377  ctiunctlemudc  12379  ctiunct  12382  ctiunctal  12383  unct  12384  ssomct  12387  nninfdclemcl  12390  nninfdclemp1  12392  nninfdc  12395  structcnvcnv  12419  setscom  12443  restid2  12575  mgmplusf  12607  grprinvlem  12626  grprinvd  12627  grpridd  12628  ismnd  12642  mhmpropd  12676  grppropd  12711  topontopon  12771  eltg3i  12809  epttop  12843  difopn  12861  uncld  12866  0nnei  12906  resttopon  12924  restabs  12928  restopnb  12934  lmcvg  12970  cnptopco  12975  cnss1  12979  cnss2  12980  cncnpi  12981  cncnp2m  12984  cnrest  12988  cnrest2  12989  cnrest2r  12990  cnptoprest  12992  cnptoprest2  12993  lmss  12999  lmff  13002  lmtopcnp  13003  lmcn  13004  txbasval  13020  upxp  13025  txcnmpt  13026  txdis1cn  13031  txlm  13032  lmcn2  13033  cnmpt11  13036  cnmpt11f  13037  cnmpt1t  13038  cnmpt12  13040  cnmpt21  13044  cnmpt21f  13045  cnmpt2t  13046  cnmpt22  13047  cnmpt22f  13048  cnmptcom  13051  hmeocnv  13060  hmeof1o  13062  hmeores  13068  txhmeo  13072  txswaphmeo  13074  isxmet2d  13101  blfvalps  13138  xblss2ps  13157  xblss2  13158  blfps  13162  blf  13163  unirnblps  13175  unirnbl  13176  isxms2  13205  bdxmet  13254  bdmet  13255  xmetxp  13260  xmettx  13263  blssioo  13298  tgioo  13299  mulcncflem  13343  dedekindeulemuub  13348  dedekindeulemub  13349  dedekindeulemloc  13350  dedekindeulemlu  13352  suplociccreex  13355  suplociccex  13356  dedekindicclemuub  13357  dedekindicclemub  13358  dedekindicclemloc  13359  dedekindicclemlu  13361  dedekindicc  13364  ivthinclemlopn  13367  ivthinclemuopn  13369  limcrcl  13380  limcmpted  13385  limccnp2lem  13398  limccnp2cntop  13399  limccoap  13400  dvrecap  13430  cosordlem  13523  logbgcd1irraplemexp  13639  logbgcd1irrap  13641  lgsneg1  13679  lgsdilem  13681  lgsdir2  13687  lgsdirprm  13688  lgsdir  13689  lgsne0  13692  lgsabs1  13693  lgsdirnn0  13701  lgsdinn0  13702  2sqlem5  13708  2sqlem7  13710  2sqlem8a  13711  2sqlem8  13712  2sqlem9  13713  bj-stand  13742  bj-charfundcALT  13804  bj-charfunbi  13806  bj-bdfindis  13942  bj-peano4  13950  strcollnfALT  13981  pwtrufal  13990  pwf1oexmid  13992  exmid1stab  13993  subctctexmid  13994  pw1nct  13996  nnsf  13998  nninfalllem1  14001  nninfall  14002  nninfsellemqall  14008  exmidsbthrlem  14014  sbthom  14018  cvgcmp2nlemabs  14024  trilpo  14035  iswomni0  14043  redcwlpo  14047  dceqnconst  14051  dcapnconst  14052  nconstwlpolem  14056  nconstwlpo  14057  neapmkvlem  14058  neapmkv  14059  taupi  14062  alsi1d  14070  alsi2d  14071  alsc1d  14072  alsc2d  14073