ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylib Unicode version

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

Proof of Theorem sylib
StepHypRef Expression
1 sylib.1 . 2  |-  ( ph  ->  ps )
2 sylib.2 . . 3  |-  ( ps  <->  ch )
32biimpi 119 . 2  |-  ( ps 
->  ch )
41, 3syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
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  390  pm4.71rd  391  imdistand  443  orcomd  703  3mix3  1137  mpjao3dan  1270  ecase23d  1313  exlimdh  1560  nexd  1577  alexnim  1612  excomim  1626  19.41  1649  equcomd  1668  nfexd  1719  sbh  1734  sbcof2  1766  sbidm  1807  sb6rf  1809  nfsbt  1927  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  eu2  2021  2euex  2064  eqcomd  2123  3eltr3g  2202  abbid  2234  neneqd  2306  eqnetrrid  2316  3netr3g  2319  necomd  2371  r19.21bi  2497  nrexdv  2502  rexlimd  2523  rabbidva  2648  elisset  2674  euind  2844  rmoan  2857  reuind  2862  2rmorex  2863  spsbc  2893  spesbc  2966  eldifad  3052  eldifbd  3053  3sstr3g  3109  sseqtrdi  3115  difindiss  3300  un00  3379  undifss  3413  ifcldcd  3477  disjpr2  3557  difprsn1  3629  diftpsn3  3631  difsnss  3636  sneqr  3657  preqr1  3665  preq12b  3667  oprcl  3699  intab  3770  riinm  3855  rintm  3875  disjiun  3894  sndisj  3895  3brtr3g  3931  trint  4011  iinexgm  4049  exmidexmid  4090  exmid01  4091  pwntru  4092  pwel  4110  exss  4119  0nelop  4140  euotd  4146  opelopabsb  4152  pwunim  4178  issod  4211  frind  4244  suctr  4313  orduniss  4317  onelini  4322  oneluni  4323  eusv2i  4346  rexxfrd  4354  rabxfrd  4360  reuhypd  4362  iunpw  4371  sucexg  4384  ordsucim  4386  ordtriexmidlem  4405  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  ordsucunielexmid  4416  orddif  4432  suc11g  4442  onintexmid  4457  reg3exmidlemwe  4463  tfisi  4471  peano1  4478  peano2  4479  finds2  4485  omsinds  4505  brrelex12  4547  brel  4561  ssrel  4597  ssrel2  4599  ssrelrel  4609  elrel  4611  xpsspw  4621  relop  4659  dmxpm  4729  opelresi  4800  ndmima  4886  poirr2  4901  xpmlem  4929  xpimasn  4957  iotass  5075  iotacl  5081  dffun5r  5105  funeu  5118  funeu2  5119  funfnd  5124  funopg  5127  funun  5137  funinsn  5142  funtp  5146  funcnvuni  5162  funcnvres2  5168  imadiflem  5172  imadif  5173  funimaexglem  5176  fneu2  5198  fnimaeq0  5214  fnmpt  5219  fun2  5266  f00  5284  f0bi  5285  foimacnv  5353  resdif  5357  f1ococnv1  5364  fv3  5412  relelfvdm  5421  nfvres  5422  dffn5im  5435  mptfvex  5474  fvmptdf  5476  fvmptdv2  5478  fndmdif  5493  dff4im  5534  fmpt  5538  fmptd  5542  fmptdf  5545  f1oresrab  5553  fcoconst  5559  fsn  5560  ftpg  5572  fsnunf  5588  resfunexg  5609  isores1  5683  riota2df  5718  acexmidlemcase  5737  brabvv  5785  funoprabg  5838  fnovim  5847  ovmpodf  5870  ovi3  5875  grprinvlem  5933  grprinvd  5934  grpridd  5935  elmpocl  5936  1stcof  6029  2ndcof  6030  fnmpo  6068  fmpoco  6081  fo2ndf  6092  f1o2ndf1  6093  disjxp1  6101  brtpos2  6116  reldmtpos  6118  dftpos3  6127  dftpos4  6128  tpostpos2  6130  tposf2  6133  tposf12  6134  tposfo  6136  tposf  6137  smores2  6159  tfrlem1  6173  tfrlem3-2d  6177  tfrlemisucaccv  6190  tfrlemibxssdm  6192  tfrlemibfn  6193  tfrlemi1  6197  tfrexlem  6199  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcldm  6228  rdgivallem  6246  rdgisucinc  6250  frecabex  6263  frecfnom  6266  frecfcllem  6269  frecsuclem  6271  omsuc  6336  nntri2  6358  nnsucuniel  6359  nnsseleq  6365  nnm00  6393  ecexr  6402  swoer  6425  elqsn0m  6465  iinerm  6469  erinxp  6471  ecinxp  6472  eroveu  6488  eroprf  6490  mapprc  6514  mapsn  6552  ixpprc  6581  ixp0  6593  resixp  6595  elixpsn  6597  dom2lem  6634  fundmen  6668  dom0  6700  xpf1o  6706  mapxpen  6710  xpmapenlem  6711  ssenen  6713  nneneq  6719  ssfilem  6737  dif1en  6741  dif1enen  6742  fin0  6747  fin0or  6748  diffitest  6749  diffisn  6755  ac6sfi  6760  fimax2gtrilemstep  6762  fimax2gtri  6763  finexdc  6764  onunsnss  6773  unsnfidcel  6777  undifdcss  6779  undifdc  6780  fiintim  6785  fisseneq  6788  fidcenumlemr  6811  sbthlemi4  6816  sbthlemi5  6817  sbthlemi9  6821  fifo  6836  suplubti  6855  supelti  6857  infmoti  6883  infisoti  6887  djulclb  6908  updjud  6935  omp1eomlem  6947  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumct  6968  finomni  6980  fodjuomnilemdc  6984  fodjum  6986  fodjuomnilemres  6988  fodjumkvlemres  7001  exmidonfinlem  7017  en2eleq  7019  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  exmidfodomrlemim  7025  acfun  7031  exmidaclem  7032  ccfunen  7047  elni2  7090  indpi  7118  distrnqg  7163  subhalfnqq  7190  enq0sym  7208  enq0ref  7209  enq0tr  7210  nqnq0pi  7214  nnnq0lem1  7222  distrnq0  7235  elinp  7250  elnp1st2nd  7252  prltlu  7263  prnmaxl  7264  prnminu  7265  prarloc  7279  nqprm  7318  appdivnq  7339  prmuloc  7342  mullocpr  7347  distrlem4prl  7360  distrlem4pru  7361  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  cauappcvgprlemopl  7422  cauappcvgprlemopu  7424  cauappcvgprlemdisj  7427  cauappcvgprlem2  7436  cauappcvgprlemlim  7437  caucvgprlemnkj  7442  caucvgprlemopl  7445  caucvgprlemopu  7447  caucvgprlemdisj  7450  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem2  7456  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemlol  7474  caucvgprprlemexbt  7482  caucvgprprlem1  7485  suplocexprlemrl  7493  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  prsrlem1  7518  gt0srpr  7524  caucvgsrlemcl  7565  caucvgsrlembound  7570  caucvgsrlemgt1  7571  suplocsrlemb  7582  suplocsrlem  7584  suplocsr  7585  ltresr  7615  nnindnn  7669  axcaucvglemcl  7671  axcaucvglemval  7673  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  sup3exmid  8679  nnind  8700  nn0supp  8987  nn0ge2m1nn  8995  zleloe  9059  zapne  9083  nn0lt2  9090  suprzclex  9107  zindd  9127  uzm1  9312  uzin  9314  elnn1uz2  9357  nn01to3  9365  divfnzn  9369  qapne  9387  xrltnsym2  9535  xaddass  9607  xleadd1a  9611  xlt2add  9618  xlesubadd  9621  iooval2  9653  icoshftf1o  9729  fztri3or  9774  fzneuz  9836  4fvwrd4  9872  elfzo0  9914  exbtwnzlemex  9982  ioom  9993  fzfig  10158  uzennn  10164  uzsinds  10170  iseqovex  10184  seq3val  10186  seqvalcd  10187  seqf  10189  seqovcd  10191  monoord2  10205  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  seq3f1olemqsum  10228  seq3f1o  10232  seq3distr  10241  expp1  10255  expcl2lemap  10260  expclzap  10273  expap0i  10280  bcval5  10464  hashinfuni  10478  hashennnuni  10480  hashnncl  10497  resunimafz0  10529  zfz1isolemiso  10537  zfz1isolem1  10538  zfz1iso  10539  seq3shft  10565  cvg1nlemcau  10711  rexanuz  10715  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemsqa  10751  resqrexlemex  10752  rersqreu  10755  caubnd2  10844  maxleast  10940  fimaxre2  10953  minmax  10956  xrmaxiflemcl  10969  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxadd  10985  xrminmax  10989  xrbdtri  11000  climreu  11021  reccn2ap  11037  iserex  11063  climcvg1nlem  11073  serf0  11076  fz1f1o  11099  summodclem3  11104  zsumdc  11108  fsum3  11111  isumz  11113  isumss  11115  isumss2  11117  fsumsersdc  11119  fsum3ser  11121  fsumsplit  11131  isumclim2  11146  isumclim3  11147  fsum2dlemstep  11158  fsumcnv  11161  fisumcom2  11162  bcxmas  11213  isumle  11219  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratz  11256  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  ef0lem  11280  mod2eq1n2dvds  11488  ndvdssub  11539  infssuzex  11554  infssuzcldc  11556  gcdsupex  11558  gcdsupcl  11559  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlembi  11605  bezoutlemeu  11607  bezoutlemle  11608  nn0seqcvgd  11634  eucalgf  11648  eucalginv  11649  lcmval  11656  prmind2  11713  dfphi2  11807  phiprmpw  11809  phimullem  11812  ennnfonelemom  11832  ennnfoneleminc  11835  ennnfonelemhf1o  11837  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemdm  11844  ennnfonelemr  11847  ennnfonelemim  11848  exmidunben  11850  ctinfom  11852  inffinp1  11853  ctinf  11854  enctlem  11856  ctiunctlemu1st  11858  ctiunctlemu2nd  11859  ctiunctlemudc  11861  ctiunct  11864  unct  11865  structcnvcnv  11886  setscom  11910  restid2  12040  topontopon  12098  eltg3i  12136  epttop  12170  difopn  12188  uncld  12193  0nnei  12233  resttopon  12251  restabs  12255  restopnb  12261  lmcvg  12297  cnptopco  12302  cnss1  12306  cnss2  12307  cncnpi  12308  cncnp2m  12311  cnrest  12315  cnrest2  12316  cnrest2r  12317  cnptoprest  12319  cnptoprest2  12320  lmss  12326  lmff  12329  lmtopcnp  12330  lmcn  12331  txbasval  12347  upxp  12352  txcnmpt  12353  txdis1cn  12358  txlm  12359  lmcn2  12360  cnmpt11  12363  cnmpt11f  12364  cnmpt1t  12365  cnmpt12  12367  cnmpt21  12371  cnmpt21f  12372  cnmpt2t  12373  cnmpt22  12374  cnmpt22f  12375  cnmptcom  12378  hmeocnv  12387  hmeof1o  12389  hmeores  12395  txhmeo  12399  txswaphmeo  12401  isxmet2d  12428  blfvalps  12465  xblss2ps  12484  xblss2  12485  blfps  12489  blf  12490  unirnblps  12502  unirnbl  12503  isxms2  12532  bdxmet  12581  bdmet  12582  xmetxp  12587  xmettx  12590  blssioo  12625  tgioo  12626  mulcncflem  12670  dedekindeulemuub  12675  dedekindeulemub  12676  dedekindeulemloc  12677  dedekindeulemlu  12679  suplociccreex  12682  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemub  12685  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicc  12691  ivthinclemlopn  12694  ivthinclemuopn  12696  limcrcl  12707  limcmpted  12712  limccnp2lem  12725  limccnp2cntop  12726  limccoap  12727  dvrecap  12757  bj-stand  12852  bj-bdfindis  13041  bj-peano4  13049  strcollnfALT  13080  pwtrufal  13088  pwf1oexmid  13090  exmid1stab  13091  subctctexmid  13092  nnsf  13095  nninfalllem1  13099  nninfall  13100  nninfsellemqall  13107  exmidsbthrlem  13113  sbthom  13117  cvgcmp2nlemabs  13123  trilpo  13132  alsi1d  13142  alsi2d  13143  alsc1d  13144  alsc2d  13145
  Copyright terms: Public domain W3C validator