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	|- ( ph -> ps )
sylib.2	|- ( ps <-> ch )

Assertion

Ref	Expression
sylib	|- ( ph -> ch )

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 |- ( ph -> ps )
2		sylib.2	. . 3 |- ( ps <-> ch )
3	2	biimpi 120	. 2 |- ( ps -> ch )
4	1, 3	syl 14	1 |- ( ph -> ch )

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  sn0disj  4127  3brtr3g  4164  trint  4246  iinexgm  4292  exmidexmid  4335  exmid01  4337  pwntru  4338  exmid1stab  4347  pwel  4360  exss  4369  0nelop  4390  euotd  4397  opelopabsb  4404  pwunim  4433  issod  4466  frind  4499  suctr  4568  orduniss  4572  onelini  4577  oneluni  4578  eusv2i  4603  rexxfrd  4611  rabxfrd  4617  reuhypd  4619  iunpw  4628  sucexg  4647  ordsucim  4649  ordtriexmidlem  4668  ontriexmidim  4671  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  ordsucunielexmid  4680  orddif  4696  suc11g  4706  onintexmid  4722  reg3exmidlemwe  4728  tfisi  4736  peano1  4743  peano2  4744  finds2  4750  omsinds  4771  brrelex12  4815  brel  4829  ssrel  4865  ssrel2  4867  ssrelrel  4877  elrel  4879  xpsspw  4889  relop  4932  dmxpm  5004  opelresi  5076  mptimass  5142  ndmima  5167  poirr2  5183  xpmlem  5211  xpimasn  5239  iotass  5358  iotacl  5365  dffun5r  5392  funeu  5405  funeu2  5406  funfnd  5411  funopg  5414  funun  5425  fununfun  5427  funinsn  5433  funtp  5437  funcnvuni  5453  funcnvres2  5459  imadiflem  5463  imadif  5464  funimaexglem  5467  fneu2  5491  fnimaeq0  5508  fnmpt  5513  ffrn  5548  fun2  5565  f00  5587  f0bi  5588  fimadmfo  5627  foimacnv  5660  resdif  5664  f1ococnv1  5671  fv3  5721  relelfvdm  5730  elfvm  5732  nfvres  5735  dffn5im  5751  mptfvex  5794  fvmptdf  5796  fvmptdv2  5798  fndmdif  5817  dff4im  5857  fmpt  5861  fmptd  5865  fmptdf  5868  f1oresrab  5876  fcoconst  5882  fsn  5883  funopsn  5894  ftpg  5902  fsnunf  5918  resfunexg  5939  mptmex  5948  isores1  6023  riota2df  6063  acexmidlemcase  6083  brabvv  6137  funoprabg  6190  fnovim  6200  ovmpodf  6223  ovi3  6229  elmpocl  6287  uchoice  6375  1stcof  6401  2ndcof  6402  opabn1stprc  6433  fnmpo  6442  fmpoco  6456  fo2ndf  6467  f1o2ndf1  6468  disjxp1  6476  fvdifsuppst  6488  fsuppeq  6491  fsuppeqg  6492  suppssrst  6505  suppssrgst  6506  brtpos2  6526  reldmtpos  6528  dftpos3  6537  dftpos4  6538  tpostpos2  6540  tposf2  6543  tposf12  6544  tposfo  6546  tposf  6547  smores2  6569  tfrlem1  6583  tfrlem3-2d  6587  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemi1  6607  tfrexlem  6609  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcldm  6638  rdgivallem  6656  rdgisucinc  6660  frecabex  6673  frecfnom  6676  frecfcllem  6679  frecsuclem  6681  omsuc  6749  nntri2  6771  nnsucuniel  6772  nnsseleq  6778  nnm00  6807  ecexr  6816  swoer  6839  elqsn0m  6881  iinerm  6885  erinxp  6887  ecinxp  6888  eroveu  6904  eroprf  6906  mapprc  6930  mapsn  6976  ixpprc  7005  ixp0  7017  resixp  7019  elixpsn  7021  dom2lem  7062  fundmen  7098  1dom1el  7111  dom0  7142  xpf1o  7148  mapxpen  7152  xpmapenlem  7153  ssenen  7156  nneneq  7162  ssfilem  7181  ssfilemd  7183  dif1en  7187  dif1enen  7188  fin0  7193  fin0or  7194  diffitest  7195  diffisn  7201  ac6sfi  7206  fimax2gtrilemstep  7209  fimax2gtri  7210  finexdc  7211  eqsndc  7214  exmidpweq  7220  pw1fin  7221  onunsnss  7228  unsnfidcel  7232  undifdcss  7234  undifdc  7235  tpfidceq  7241  fiintim  7242  fisseneq  7246  fidcenumlemr  7277  sbthlemi4  7282  sbthlemi5  7283  sbthlemi9  7287  fifo  7319  2omap  7324  suplubti  7346  supelti  7348  infmoti  7374  infisoti  7378  djulclb  7401  updjud  7428  omp1eomlem  7440  0ct  7453  ctmlemr  7454  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumct  7461  nninfninc  7469  nnnninfeq2  7475  finomni  7486  fodjuomnilemdc  7490  fodjum  7492  fodjuomnilemres  7494  fodjumkvlemres  7505  omniwomnimkv  7513  nninfwlporlem  7519  nninfwlpoimlemginf  7522  nninfwlpoim  7525  nninfinfwlpo  7526  ficardon  7540  pr2cv1  7547  exmidonfinlem  7551  en2eleq  7553  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemim  7559  finacn  7566  acfun  7569  exmidaclem  7570  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  pw1if  7590  pw1on  7591  papsym  7618  papcotr  7619  dftap2  7623  2omotaplemst  7630  exmidapne  7632  ccfunen  7636  cc1  7637  cc2lem  7638  cc2  7639  cc3  7640  acnccim  7644  elni2  7687  indpi  7715  distrnqg  7760  subhalfnqq  7787  enq0sym  7805  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  nnnq0lem1  7819  distrnq0  7832  elinp  7847  elnp1st2nd  7849  prltlu  7860  prnmaxl  7861  prnminu  7862  prarloc  7876  nqprm  7915  appdivnq  7936  prmuloc  7939  mullocpr  7944  distrlem4prl  7957  distrlem4pru  7958  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemdisj  8024  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  caucvgprlemnkj  8039  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemdisj  8047  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemlol  8071  caucvgprprlemexbt  8079  caucvgprprlem1  8082  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  prsrlem1  8115  gt0srpr  8121  caucvgsrlemcl  8162  caucvgsrlembound  8167  caucvgsrlemgt1  8168  suplocsrlemb  8179  suplocsrlem  8181  suplocsr  8182  ltresr  8212  nnindnn  8266  axcaucvglemcl  8268  axcaucvglemval  8270  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  sup3exmid  9295  indconst0  9311  indconst1  9312  nnind  9329  nn0supp  9630  nn0ge2m1nn  9638  zleloe  9702  zapne  9730  nn0lt2  9738  suprzclex  9755  zindd  9775  uzm1  9969  uzin  9971  infregelbex  10014  elnn1uz2  10023  nn01to3  10033  divfnzn  10037  qapne  10055  irraddap  10063  xrltnsym2  10213  xaddass  10288  xleadd1a  10292  xlt2add  10299  xlesubadd  10302  iooval2  10334  icoshftf1o  10410  fztri3or  10460  fzneuz  10525  4fvwrd4  10564  elfzo0  10610  infssuzex  10683  infssuzcldc  10685  infssfzcldc  10686  infssfzledc  10687  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  exbtwnzlemex  10701  ioom  10712  fzfig  10888  uzennn  10894  uzsinds  10902  iseqovex  10916  seq3val  10918  seqvalcd  10919  seqf  10922  seqovcd  10925  monoord2  10944  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seq3f1olemqsum  10971  seq3f1o  10975  seqf1og  10979  seq3distr  10990  expp1  11004  expcl2lemap  11009  expclzap  11022  expap0i  11029  nn0ltexp2  11169  bcval5  11223  hashinfuni  11238  hashennnuni  11240  hashnncl  11256  resunimafz0  11296  hashf1lem2  11308  hashf1  11309  zfz1isolemiso  11313  zfz1isolem1  11314  zfz1iso  11315  wrdsymb0  11359  wrdlen1  11364  ccat1st1st  11431  swrdrlen  11455  pfxid  11480  pfxwrdsymbg  11484  pfxtrcfv  11487  pfxccat1  11496  pfxpfxid  11503  pfxcctswrd  11504  swrdccatin1  11519  pfxccatin12  11527  pfxccatid  11535  seq3shft  11625  cvg1nlemcau  11772  rexanuz  11776  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  rersqreu  11816  caubnd2  11906  maxleast  12002  fimaxre2  12016  minmax  12020  xrmaxiflemcl  12036  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  climreu  12088  reccn2ap  12104  iserex  12130  climcvg1nlem  12140  serf0  12143  fz1f1o  12166  summodclem3  12172  zsumdc  12176  fsum3  12179  isumz  12181  isumss  12183  isumss2  12185  fsumsersdc  12187  fsum3ser  12189  fsumsplit  12199  isumclim2  12214  isumclim3  12215  fsum2dlemstep  12226  fsumcnv  12229  fisumcom2  12230  bcxmas  12281  isumle  12287  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratz  12324  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  zproddc  12371  prod1dc  12378  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  fprodcllemf  12405  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  fprodle  12432  ef0lem  12452  fsumdvds  12634  mod2eq1n2dvds  12671  ndvdssub  12722  bitsfzolem  12746  bitsfzo  12747  bitsinv1  12754  gcdsupex  12759  gcdsupcl  12760  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlembi  12807  bezoutlemeu  12809  bezoutlemle  12810  uzwodc  12839  nnwofdc  12840  nnwosdc  12841  nninfctlemfo  12842  nninfct  12843  nn0seqcvgd  12844  eucalgf  12858  eucalginv  12859  lcmval  12866  prmind2  12923  dfphi2  13027  phiprmpw  13029  phimullem  13032  eulerthlem1  13034  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  eulerth  13040  phisum  13048  odzcllem  13050  odzdvds  13053  pythagtriplem19  13090  pclemub  13095  pcprecl  13097  pceu  13103  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxqcl  13120  pcge0  13121  pcdvdsb  13128  pceq0  13130  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcmptcl  13150  pcmpt  13151  pcmptdvds  13153  fldivp1  13156  qexpz  13160  pockthlem  13164  pockthg  13165  prmunb  13170  1arith  13175  4sqlemffi  13204  4sqlem17  13215  4sqlem18  13216  4sqlem19  13217  prmlem1a  13250  ballotfilemcdc  13281  ballotfilem2  13286  ballotfilemfp1  13289  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfmpn  13292  ballotfilemefi  13295  ballotfilemiex  13302  ballotfilemro  13324  ennnfonelemom  13357  ennnfoneleminc  13360  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemdm  13369  ennnfonelemr  13372  ennnfonelemim  13373  exmidunben  13375  ctinfom  13377  inffinp1  13378  ctinf  13379  enctlem  13381  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunct  13389  ctiunctal  13390  unct  13391  ssomct  13394  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  structcnvcnv  13426  setscom  13450  relelbasov  13474  ressbas2d  13481  ressval3d  13485  ressabsg  13489  restid2  13661  imasaddfnlemg  13694  quslem  13704  ercpbl  13711  fnpr2ob  13720  mgmplusf  13745  grpinvalem  13764  grpinva  13765  grprida  13766  fngzsum  13767  gzsumvalx  13768  gzsum0  13772  gzsumval2  13773  ismnd  13791  mhmpropd  13832  grppropd  13881  grpsubf  13943  dfgrp3mlem  13962  mulgnn0p1  13995  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgnn0dir  14014  mulgnn0ass  14020  submmulg  14028  issubg2m  14051  issubg4m  14055  ghmmulg  14118  ghmrn  14119  gsumvalfi  14242  gzsumgsum  14245  gsumf1ofi  14250  gsummptfidmsplit  14254  gsumresfi  14263  gsummhmfi  14264  gsumressfi  14267  gsum2d2fi  14274  gsumcom2fi  14275  lringuplu  14612  rrgsupp  14683  opprdrng  14729  lmodscaf  14756  lssintclm  14830  lspun0  14871  lidlbas  14924  psrbagconcl  15173  gsumbagdiaglem  15175  psr1clfi  15198  topontopon  15246  eltg3i  15282  epttop  15316  difopn  15334  uncld  15339  0nnei  15379  resttopon  15397  restabs  15401  restopnb  15407  lmcvg  15443  cnptopco  15448  cnss1  15452  cnss2  15453  cncnpi  15454  cncnp2m  15457  cnrest  15461  cnrest2  15462  cnrest2r  15463  cnptoprest  15465  cnptoprest2  15466  lmss  15472  lmff  15475  lmtopcnp  15476  lmcn  15477  txbasval  15493  upxp  15498  txcnmpt  15499  txdis1cn  15504  txlm  15505  lmcn2  15506  cnmpt11  15509  cnmpt11f  15510  cnmpt1t  15511  cnmpt12  15513  cnmpt21  15517  cnmpt21f  15518  cnmpt2t  15519  cnmpt22  15520  cnmpt22f  15521  cnmptcom  15524  hmeocnv  15533  hmeof1o  15535  hmeores  15541  txhmeo  15545  txswaphmeo  15547  isxmet2d  15574  blfvalps  15611  xblss2ps  15630  xblss2  15631  blfps  15635  blf  15636  unirnblps  15648  unirnbl  15649  isxms2  15678  bdxmet  15727  bdmet  15728  xmetxp  15733  xmettx  15736  blssioo  15779  tgioo  15780  mulcncflem  15833  divcncfap  15840  dedekindeulemuub  15843  dedekindeulemub  15844  dedekindeulemloc  15845  dedekindeulemlu  15847  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemub  15853  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthdich  15879  limcrcl  15884  limcmpted  15889  limccnp2lem  15902  limccnp2cntop  15903  limccoap  15904  dvrecap  15939  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  plyco  15985  plycj  15987  plyrecj  15989  dvply1  15991  dvply2g  15992  cosordlem  16077  logbgcd1irraplemexp  16204  logbgcd1irrap  16206  zprmlogbaplem2  16216  zprmlogbaplem3  16217  birthdaylem2  16226  birthdaylem3  16227  chtqge0  16247  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  chtqwordi  16263  ppiqltx  16281  bposlem2  16312  lgsneg1  16349  lgsdilem  16351  lgsdir2  16357  lgsdirprm  16358  lgsdir  16359  lgsne0  16362  lgsabs1  16363  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1f1o  16384  gausslemma2dlem4  16388  lgseisenlem1  16394  lgsquadlem3  16403  2lgslem1a  16412  2sqlem5  16443  2sqlem7  16445  2sqlem8a  16446  2sqlem8  16447  2sqlem9  16448  gropeld  16495  grstructeld2dom  16496  uhgrm  16524  upgrm  16546  upgr1een  16570  uhgredgm  16582  edgupgren  16587  edgumgren  16588  edgusgren  16609  ausgrusgrben  16614  umgr2edg1  16655  usgredg2vlem1  16668  uhgr0enedgfi  16682  subupgr  16719  vtxedgfi  16735  vtxlpfi  16736  vtxdumgrfival  16744  vtxd0nedgbfi  16745  1hevtxdg0fi  16753  p1evtxdeqfilem  16757  wlkvtxm  16786  g0wlk0  16816  wlkres  16825  trlreslem  16835  clwwlkccatlem  16846  clwwlknnn  16858  trlsegvdeglem6  16911  eupth2lem3lem3fi  16916  eupth2lem3lem7fi  16920  eulerpathum  16927  dichmul0or  16965  bj-stand  16981  bj-charfundcALT  17040  bj-charfunbi  17042  bj-bdfindis  17178  bj-peano4  17186  strcollnfALT  17217  pw1map  17230  pwtrufal  17232  pwf1oexmid  17234  subctctexmid  17235  pw1nct  17238  stnot  17244  wexmiddc  17247  nnsf  17254  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264  nnnninfen  17270  exmidsbthrlem  17273  sbthom  17277  repiecef  17283  cvgcmp2nlemabs  17287  trilpo  17299  iswomni0  17308  redcwlpo  17312  dceqnconst  17317  dcapnconst  17318  nconstwlpolem  17322  nconstwlpo  17323  neapmkvlem  17324  neapmkv  17325  ltlenmkv  17327  taupi  17330  als1d  17340  als2d  17341  rals1d  17342  rals2d  17343  alseu1d  17376  alseu2d  17377  ralseu1d  17378  ralseu2d  17379  dfalseu2  17384