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  388  pm4.71rd  389  imdistand  441  orcomd  701  3mix3  1135  mpjao3dan  1268  ecase23d  1311  exlimdh  1558  nexd  1575  alexnim  1610  excomim  1624  19.41  1647  equcomd  1666  nfexd  1717  sbh  1732  sbcof2  1764  sbidm  1805  sb6rf  1807  nfsbt  1925  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  eu2  2019  2euex  2062  eqcomd  2121  3eltr3g  2200  abbid  2232  neneqd  2304  eqnetrrid  2314  3netr3g  2317  necomd  2369  r19.21bi  2495  nrexdv  2500  rexlimd  2521  rabbidva  2646  elisset  2672  euind  2842  rmoan  2855  reuind  2860  2rmorex  2861  spsbc  2891  spesbc  2964  eldifad  3050  eldifbd  3051  3sstr3g  3107  syl6sseq  3113  difindiss  3298  un00  3377  undifss  3411  ifcldcd  3475  disjpr2  3555  difprsn1  3627  diftpsn3  3629  difsnss  3634  sneqr  3655  preqr1  3663  preq12b  3665  oprcl  3697  intab  3768  riinm  3853  rintm  3873  disjiun  3892  sndisj  3893  3brtr3g  3929  trint  4009  iinexgm  4047  exmidexmid  4088  exmid01  4089  pwntru  4090  pwel  4108  exss  4117  0nelop  4138  euotd  4144  opelopabsb  4150  pwunim  4176  issod  4209  frind  4242  suctr  4311  orduniss  4315  onelini  4320  oneluni  4321  eusv2i  4344  rexxfrd  4352  rabxfrd  4358  reuhypd  4360  iunpw  4369  sucexg  4382  ordsucim  4384  ordtriexmidlem  4403  ordtri2or2exmidlem  4409  onsucelsucexmidlem  4412  ordsucunielexmid  4414  orddif  4430  suc11g  4440  onintexmid  4455  reg3exmidlemwe  4461  tfisi  4469  peano1  4476  peano2  4477  finds2  4483  omsinds  4503  brrelex12  4545  brel  4559  ssrel  4595  ssrel2  4597  ssrelrel  4607  elrel  4609  xpsspw  4619  relop  4657  dmxpm  4727  opelresi  4798  ndmima  4884  poirr2  4899  xpmlem  4927  xpimasn  4955  iotass  5073  iotacl  5079  dffun5r  5103  funeu  5116  funeu2  5117  funfnd  5122  funopg  5125  funun  5135  funinsn  5140  funtp  5144  funcnvuni  5160  funcnvres2  5166  imadiflem  5170  imadif  5171  funimaexglem  5174  fneu2  5196  fnimaeq0  5212  fnmpt  5217  fun2  5264  f00  5282  f0bi  5283  foimacnv  5351  resdif  5355  f1ococnv1  5362  fv3  5410  relelfvdm  5419  nfvres  5420  dffn5im  5433  mptfvex  5472  fvmptdf  5474  fvmptdv2  5476  fndmdif  5491  dff4im  5532  fmpt  5536  fmptd  5540  fmptdf  5543  f1oresrab  5551  fcoconst  5557  fsn  5558  ftpg  5570  fsnunf  5586  resfunexg  5607  isores1  5681  riota2df  5716  acexmidlemcase  5735  brabvv  5783  funoprabg  5836  fnovim  5845  ovmpodf  5868  ovi3  5873  grprinvlem  5931  grprinvd  5932  grpridd  5933  elmpocl  5934  1stcof  6027  2ndcof  6028  fnmpo  6066  fmpoco  6079  fo2ndf  6090  f1o2ndf1  6091  disjxp1  6099  brtpos2  6114  reldmtpos  6116  dftpos3  6125  dftpos4  6126  tpostpos2  6128  tposf2  6131  tposf12  6132  tposfo  6134  tposf  6135  smores2  6157  tfrlem1  6171  tfrlem3-2d  6175  tfrlemisucaccv  6188  tfrlemibxssdm  6190  tfrlemibfn  6191  tfrlemi1  6195  tfrexlem  6197  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemaccex  6211  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemaccex  6224  tfrcldm  6226  rdgivallem  6244  rdgisucinc  6248  frecabex  6261  frecfnom  6264  frecfcllem  6267  frecsuclem  6269  omsuc  6334  nntri2  6356  nnsucuniel  6357  nnsseleq  6363  nnm00  6391  ecexr  6400  swoer  6423  elqsn0m  6463  iinerm  6467  erinxp  6469  ecinxp  6470  eroveu  6486  eroprf  6488  mapprc  6512  mapsn  6550  ixpprc  6579  ixp0  6591  resixp  6593  elixpsn  6595  dom2lem  6632  fundmen  6666  dom0  6698  xpf1o  6704  mapxpen  6708  xpmapenlem  6709  ssenen  6711  nneneq  6717  ssfilem  6735  dif1en  6739  dif1enen  6740  fin0  6745  fin0or  6746  diffitest  6747  diffisn  6753  ac6sfi  6758  fimax2gtrilemstep  6760  fimax2gtri  6761  finexdc  6762  onunsnss  6771  unsnfidcel  6775  undifdcss  6777  undifdc  6778  fiintim  6783  fisseneq  6786  fidcenumlemr  6809  sbthlemi4  6814  sbthlemi5  6815  sbthlemi9  6819  fifo  6834  suplubti  6853  supelti  6855  infmoti  6881  infisoti  6885  djulclb  6906  updjud  6933  omp1eomlem  6945  0ct  6958  ctmlemr  6959  ctssdclemn0  6961  ctssdccl  6962  ctssdc  6964  enumct  6966  finomni  6978  fodjuomnilemdc  6982  fodjum  6984  fodjuomnilemres  6986  fodjumkvlemres  6999  en2eleq  7015  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemim  7021  acfun  7027  exmidaclem  7028  ccfunen  7043  elni2  7086  indpi  7114  distrnqg  7159  subhalfnqq  7186  enq0sym  7204  enq0ref  7205  enq0tr  7206  nqnq0pi  7210  nnnq0lem1  7218  distrnq0  7231  elinp  7246  elnp1st2nd  7248  prltlu  7259  prnmaxl  7260  prnminu  7261  prarloc  7275  nqprm  7314  appdivnq  7335  prmuloc  7338  mullocpr  7343  distrlem4prl  7356  distrlem4pru  7357  ltexprlemm  7372  ltexprlemopl  7373  ltexprlemopu  7375  cauappcvgprlemopl  7418  cauappcvgprlemopu  7420  cauappcvgprlemdisj  7423  cauappcvgprlem2  7432  cauappcvgprlemlim  7433  caucvgprlemnkj  7438  caucvgprlemopl  7441  caucvgprlemopu  7443  caucvgprlemdisj  7446  caucvgprlemcl  7448  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlem2  7452  caucvgprprlemcbv  7459  caucvgprprlemval  7460  caucvgprprlemlol  7470  caucvgprprlemexbt  7478  caucvgprprlem1  7481  suplocexprlemrl  7489  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  suplocexprlemlub  7496  prsrlem1  7514  gt0srpr  7520  caucvgsrlemcl  7561  caucvgsrlembound  7566  caucvgsrlemgt1  7567  suplocsrlemb  7578  suplocsrlem  7580  suplocsr  7581  ltresr  7611  nnindnn  7665  axcaucvglemcl  7667  axcaucvglemval  7669  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  axpre-suploc  7674  sup3exmid  8672  nnind  8693  nn0supp  8980  nn0ge2m1nn  8988  zleloe  9052  zapne  9076  nn0lt2  9083  suprzclex  9100  zindd  9120  uzm1  9305  uzin  9307  elnn1uz2  9350  nn01to3  9358  divfnzn  9362  qapne  9380  xrltnsym2  9520  xaddass  9592  xleadd1a  9596  xlt2add  9603  xlesubadd  9606  iooval2  9638  icoshftf1o  9714  fztri3or  9759  fzneuz  9821  4fvwrd4  9857  elfzo0  9899  exbtwnzlemex  9967  ioom  9978  fzfig  10143  uzennn  10149  uzsinds  10155  iseqovex  10169  seq3val  10171  seqvalcd  10172  seqf  10174  seqovcd  10176  monoord2  10190  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  seq3f1olemqsum  10213  seq3f1o  10217  seq3distr  10226  expp1  10240  expcl2lemap  10245  expclzap  10258  expap0i  10265  bcval5  10449  hashinfuni  10463  hashennnuni  10465  hashnncl  10482  resunimafz0  10514  zfz1isolemiso  10522  zfz1isolem1  10523  zfz1iso  10524  seq3shft  10550  cvg1nlemcau  10696  rexanuz  10700  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemsqa  10736  resqrexlemex  10737  rersqreu  10740  caubnd2  10829  maxleast  10925  fimaxre2  10938  minmax  10941  xrmaxiflemcl  10954  xrmaxiflemab  10956  xrmaxiflemlub  10957  xrmaxadd  10970  xrminmax  10974  xrbdtri  10985  climreu  11006  reccn2ap  11022  iserex  11048  climcvg1nlem  11058  serf0  11061  fz1f1o  11084  summodclem3  11089  zsumdc  11093  fsum3  11096  isumz  11098  isumss  11100  isumss2  11102  fsumsersdc  11104  fsum3ser  11106  fsumsplit  11116  isumclim2  11131  isumclim3  11132  fsum2dlemstep  11143  fsumcnv  11146  fisumcom2  11147  bcxmas  11198  isumle  11204  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  cvgratz  11241  mertenslemub  11243  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  ef0lem  11265  mod2eq1n2dvds  11472  ndvdssub  11523  infssuzex  11538  infssuzcldc  11540  gcdsupex  11542  gcdsupcl  11543  bezoutlemnewy  11580  bezoutlemmain  11582  bezoutlembi  11589  bezoutlemeu  11591  bezoutlemle  11592  nn0seqcvgd  11618  eucalgf  11632  eucalginv  11633  lcmval  11640  prmind2  11697  dfphi2  11791  phiprmpw  11793  phimullem  11796  ennnfonelemom  11816  ennnfoneleminc  11819  ennnfonelemhf1o  11821  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemdm  11828  ennnfonelemr  11831  ennnfonelemim  11832  exmidunben  11834  ctinfom  11836  inffinp1  11837  ctinf  11838  enctlem  11840  ctiunctlemu1st  11842  ctiunctlemu2nd  11843  ctiunctlemudc  11845  ctiunct  11848  unct  11849  structcnvcnv  11870  setscom  11894  restid2  12024  topontopon  12082  eltg3i  12120  epttop  12154  difopn  12172  uncld  12177  0nnei  12217  resttopon  12235  restabs  12239  restopnb  12245  lmcvg  12281  cnptopco  12286  cnss1  12290  cnss2  12291  cncnpi  12292  cncnp2m  12295  cnrest  12299  cnrest2  12300  cnrest2r  12301  cnptoprest  12303  cnptoprest2  12304  lmss  12310  lmff  12313  lmtopcnp  12314  lmcn  12315  txbasval  12331  upxp  12336  txcnmpt  12337  txdis1cn  12342  txlm  12343  lmcn2  12344  cnmpt11  12347  cnmpt11f  12348  cnmpt1t  12349  cnmpt12  12351  cnmpt21  12355  cnmpt21f  12356  cnmpt2t  12357  cnmpt22  12358  cnmpt22f  12359  cnmptcom  12362  hmeocnv  12371  hmeof1o  12373  hmeores  12379  txhmeo  12383  txswaphmeo  12385  isxmet2d  12412  blfvalps  12449  xblss2ps  12468  xblss2  12469  blfps  12473  blf  12474  unirnblps  12486  unirnbl  12487  isxms2  12516  bdxmet  12565  bdmet  12566  xmetxp  12571  xmettx  12574  blssioo  12609  tgioo  12610  mulcncflem  12654  dedekindeulemuub  12659  dedekindeulemub  12660  dedekindeulemloc  12661  dedekindeulemlu  12663  suplociccreex  12666  suplociccex  12667  dedekindicclemuub  12668  dedekindicclemub  12669  dedekindicclemloc  12670  dedekindicclemlu  12672  dedekindicc  12675  ivthinclemlopn  12678  ivthinclemuopn  12680  limcrcl  12691  limcmpted  12696  limccnp2lem  12709  limccnp2cntop  12710  limccoap  12711  dvrecap  12741  bj-stand  12779  bj-bdfindis  12968  bj-peano4  12976  strcollnfALT  13007  pwtrufal  13015  pwf1oexmid  13017  exmid1stab  13018  subctctexmid  13019  nnsf  13022  nninfalllem1  13026  nninfall  13027  nninfsellemqall  13034  exmidsbthrlem  13040  sbthom  13044  cvgcmp2nlemabs  13050  trilpo  13059  alsi1d  13069  alsi2d  13070  alsc1d  13071  alsc2d  13072
  Copyright terms: Public domain W3C validator