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  6527  reldmtpos  6529  dftpos3  6538  dftpos4  6539  tpostpos2  6541  tposf2  6544  tposf12  6545  tposfo  6547  tposf  6548  smores2  6570  tfrlem1  6584  tfrlem3-2d  6588  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemi1  6608  tfrexlem  6610  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcldm  6639  rdgivallem  6657  rdgisucinc  6661  frecabex  6674  frecfnom  6677  frecfcllem  6680  frecsuclem  6682  omsuc  6750  nntri2  6772  nnsucuniel  6773  nnsseleq  6779  nnm00  6808  ecexr  6817  swoer  6840  elqsn0m  6882  iinerm  6886  erinxp  6888  ecinxp  6889  eroveu  6905  eroprf  6907  mapprc  6931  mapsn  6978  ixpprc  7007  ixp0  7019  resixp  7021  elixpsn  7023  dom2lem  7064  fundmen  7100  1dom1el  7113  dom0  7144  xpf1o  7150  mapxpen  7154  xpmapenlem  7155  ssenen  7158  nneneq  7164  ssfilem  7183  ssfilemd  7185  dif1en  7189  dif1enen  7190  fin0  7195  fin0or  7196  diffitest  7197  diffisn  7203  ac6sfi  7208  fimax2gtrilemstep  7211  fimax2gtri  7212  finexdc  7213  eqsndc  7216  exmidpweq  7222  pw1fin  7223  onunsnss  7230  unsnfidcel  7234  undifdcss  7236  undifdc  7237  tpfidceq  7243  fiintim  7244  fisseneq  7248  fidcenumlemr  7279  sbthlemi4  7284  sbthlemi5  7285  sbthlemi9  7289  fndmfifsupp  7303  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  9628  nn0ge2m1nn  9636  zleloe  9700  zapne  9728  nn0lt2  9736  suprzclex  9754  zindd  9774  uzm1  9968  uzin  9970  infregelbex  10013  elnn1uz2  10022  nn01to3  10032  divfnzn  10036  qapne  10054  irraddap  10062  xrltnsym2  10212  xaddass  10287  xleadd1a  10291  xlt2add  10298  xlesubadd  10301  iooval2  10333  icoshftf1o  10409  fztri3or  10459  fzneuz  10524  4fvwrd4  10563  elfzo0  10609  infssuzex  10682  infssuzcldc  10684  infssfzcldc  10685  infssfzledc  10686  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  exbtwnzlemex  10700  ioom  10711  fzfig  10887  uzennn  10893  uzsinds  10901  iseqovex  10915  seq3val  10917  seqvalcd  10918  seqf  10921  seqovcd  10924  monoord2  10943  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1olemqsum  10970  seq3f1o  10974  seqf1og  10978  seq3distr  10989  expp1  11003  expcl2lemap  11008  expclzap  11021  expap0i  11028  nn0ltexp2  11168  bcval5  11222  hashinfuni  11237  hashennnuni  11239  hashnncl  11255  resunimafz0  11295  hashf1lem2  11307  hashf1  11308  zfz1isolemiso  11312  zfz1isolem1  11313  zfz1iso  11314  wrdsymb0  11358  wrdlen1  11363  ccat1st1st  11430  swrdrlen  11454  pfxid  11479  pfxwrdsymbg  11483  pfxtrcfv  11486  pfxccat1  11495  pfxpfxid  11502  pfxcctswrd  11503  swrdccatin1  11518  pfxccatin12  11526  pfxccatid  11534  seq3shft  11624  cvg1nlemcau  11771  rexanuz  11775  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  rersqreu  11815  caubnd2  11905  maxleast  12001  fimaxre2  12015  minmax  12019  xrmaxiflemcl  12035  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxadd  12051  xrminmax  12055  xrbdtri  12066  climreu  12087  reccn2ap  12103  iserex  12129  climcvg1nlem  12139  serf0  12142  fz1f1o  12165  summodclem3  12171  zsumdc  12175  fsum3  12178  isumz  12180  isumss  12182  isumss2  12184  fsumsersdc  12186  fsum3ser  12188  fsumsplit  12198  isumclim2  12213  isumclim3  12214  fsum2dlemstep  12225  fsumcnv  12228  fisumcom2  12229  bcxmas  12280  isumle  12286  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratz  12323  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  zproddc  12370  prod1dc  12377  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  fprodcl2lem  12396  fprodcllemf  12404  fprod2dlemstep  12413  fprodcnv  12416  fprodcom2fi  12417  fprodle  12431  ef0lem  12451  fsumdvds  12633  mod2eq1n2dvds  12670  ndvdssub  12721  bitsfzolem  12745  bitsfzo  12746  bitsinv1  12753  gcdsupex  12758  gcdsupcl  12759  bezoutlemnewy  12797  bezoutlemmain  12799  bezoutlembi  12806  bezoutlemeu  12808  bezoutlemle  12809  uzwodc  12838  nnwofdc  12839  nnwosdc  12840  nninfctlemfo  12841  nninfct  12842  nn0seqcvgd  12843  eucalgf  12857  eucalginv  12858  lcmval  12865  prmind2  12922  dfphi2  13026  phiprmpw  13028  phimullem  13031  eulerthlem1  13033  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  eulerth  13039  phisum  13047  odzcllem  13049  odzdvds  13052  pythagtriplem19  13089  pclemub  13094  pcprecl  13096  pceu  13102  pcqmul  13110  pcqcl  13113  pcxnn0cl  13117  pcxqcl  13119  pcge0  13120  pcdvdsb  13127  pceq0  13129  pcneg  13132  pcdvdstr  13134  pcgcd1  13135  pc2dvds  13137  pcz  13139  pcprmpw2  13140  pcaddlem  13146  pcadd  13147  pcmptcl  13149  pcmpt  13150  pcmptdvds  13152  fldivp1  13155  qexpz  13159  pockthlem  13163  pockthg  13164  prmunb  13169  1arith  13174  4sqlemffi  13203  4sqlem17  13214  4sqlem18  13215  4sqlem19  13216  prmlem1a  13249  ballotfilemcdc  13280  ballotfilem2  13285  ballotfilemfp1  13288  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfmpn  13291  ballotfilemefi  13294  ballotfilemiex  13301  ballotfilemro  13323  ennnfonelemom  13356  ennnfoneleminc  13359  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemdm  13368  ennnfonelemr  13371  ennnfonelemim  13372  exmidunben  13374  ctinfom  13376  inffinp1  13377  ctinf  13378  enctlem  13380  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunct  13388  ctiunctal  13389  unct  13390  ssomct  13393  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  structcnvcnv  13425  setscom  13449  relelbasov  13473  ressbas2d  13480  ressval3d  13484  ressabsg  13488  restid2  13660  imasaddfnlemg  13693  quslem  13703  ercpbl  13710  fnpr2ob  13719  mgmplusf  13744  grpinvalem  13763  grpinva  13764  grprida  13765  fngzsum  13766  gzsumvalx  13767  gzsum0  13771  gzsumval2  13772  ismnd  13790  mhmpropd  13831  grppropd  13880  grpsubf  13942  dfgrp3mlem  13961  mulgnn0p1  13994  mulgnn0subcl  13996  mulgsubcl  13997  mulgneg  14001  mulgnn0dir  14013  mulgnn0ass  14019  submmulg  14027  issubg2m  14050  issubg4m  14054  ghmmulg  14117  ghmrn  14118  gsumvalfi  14241  gzsumgsum  14244  gsumf1ofi  14249  gsummptfidmsplit  14253  gsumresfi  14262  gsummhmfi  14263  gsumressfi  14266  gsum2d2fi  14273  gsumcom2fi  14274  lringuplu  14611  rrgsupp  14682  opprdrng  14728  lmodscaf  14755  lssintclm  14829  lspun0  14870  lidlbas  14923  psrbagconcl  15176  psrbagmax  15183  gsumbagdiaglem  15184  psr1clfi  15207  mplsubgfilemcl  15232  mplsubgfileminv  15233  topontopon  15263  eltg3i  15299  epttop  15333  difopn  15351  uncld  15356  0nnei  15396  resttopon  15414  restabs  15418  restopnb  15424  lmcvg  15460  cnptopco  15465  cnss1  15469  cnss2  15470  cncnpi  15471  cncnp2m  15474  cnrest  15478  cnrest2  15479  cnrest2r  15480  cnptoprest  15482  cnptoprest2  15483  lmss  15489  lmff  15492  lmtopcnp  15493  lmcn  15494  txbasval  15510  upxp  15515  txcnmpt  15516  txdis1cn  15521  txlm  15522  lmcn2  15523  cnmpt11  15526  cnmpt11f  15527  cnmpt1t  15528  cnmpt12  15530  cnmpt21  15534  cnmpt21f  15535  cnmpt2t  15536  cnmpt22  15537  cnmpt22f  15538  cnmptcom  15541  hmeocnv  15550  hmeof1o  15552  hmeores  15558  txhmeo  15562  txswaphmeo  15564  isxmet2d  15591  blfvalps  15628  xblss2ps  15647  xblss2  15648  blfps  15652  blf  15653  unirnblps  15665  unirnbl  15666  isxms2  15695  bdxmet  15744  bdmet  15745  xmetxp  15750  xmettx  15753  blssioo  15796  tgioo  15797  mulcncflem  15850  divcncfap  15857  dedekindeulemuub  15860  dedekindeulemub  15861  dedekindeulemloc  15862  dedekindeulemlu  15864  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemub  15870  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthdich  15896  limcrcl  15901  limcmpted  15906  limccnp2lem  15919  limccnp2cntop  15920  limccoap  15921  dvrecap  15956  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plyco  16002  plycj  16004  plyrecj  16006  dvply1  16008  dvply2g  16009  cosordlem  16094  logbgcd1irraplemexp  16221  logbgcd1irrap  16223  zprmlogbaplem2  16233  zprmlogbaplem3  16234  birthdaylem2  16243  birthdaylem3  16244  chtqge0  16264  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  chtqwordi  16280  ppiqltx  16298  bposlem2  16329  lgsneg1  16366  lgsdilem  16368  lgsdir2  16374  lgsdirprm  16375  lgsdir  16376  lgsne0  16379  lgsabs1  16380  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1f1o  16401  gausslemma2dlem4  16405  lgseisenlem1  16411  lgsquadlem3  16420  2lgslem1a  16429  2sqlem5  16460  2sqlem7  16462  2sqlem8a  16463  2sqlem8  16464  2sqlem9  16465  gropeld  16512  grstructeld2dom  16513  uhgrm  16541  upgrm  16563  upgr1een  16587  uhgredgm  16599  edgupgren  16604  edgumgren  16605  edgusgren  16626  ausgrusgrben  16631  umgr2edg1  16672  usgredg2vlem1  16685  uhgr0enedgfi  16699  subupgr  16736  vtxedgfi  16752  vtxlpfi  16753  vtxdumgrfival  16761  vtxd0nedgbfi  16762  1hevtxdg0fi  16770  p1evtxdeqfilem  16774  wlkvtxm  16803  g0wlk0  16833  wlkres  16842  trlreslem  16852  clwwlkccatlem  16863  clwwlknnn  16875  trlsegvdeglem6  16928  eupth2lem3lem3fi  16933  eupth2lem3lem7fi  16937  eulerpathum  16944  dichmul0or  16982  bj-stand  16998  bj-charfundcALT  17057  bj-charfunbi  17059  bj-bdfindis  17195  bj-peano4  17203  strcollnfALT  17234  pw1map  17247  pwtrufal  17249  pwf1oexmid  17251  subctctexmid  17252  pw1nct  17255  stnot  17261  wexmiddc  17264  nnsf  17271  nninfalllem1  17274  nninfall  17275  nninfsellemqall  17281  nnnninfen  17287  exmidsbthrlem  17290  sbthom  17294  repiecef  17300  cvgcmp2nlemabs  17304  trilpo  17316  iswomni0  17325  redcwlpo  17329  dceqnconst  17334  dcapnconst  17335  nconstwlpolem  17339  nconstwlpo  17340  neapmkvlem  17341  neapmkv  17342  ltlenmkv  17344  taupi  17347  als1d  17357  als2d  17358  rals1d  17359  rals2d  17360  alseu1d  17393  alseu2d  17394  ralseu1d  17395  ralseu2d  17396  dfalseu2  17401