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-1 5  ax-2 6  ax-mp 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  264  pm4.71d  386  pm4.71rd  387  imdistand  437  orcomd  684  3mix3  1115  mpjao3dan  1244  ecase23d  1287  exlimdh  1533  nexd  1550  alexnim  1585  excomim  1599  19.41  1622  equcomd  1641  nfexd  1692  sbh  1707  sbcof2  1739  sbidm  1780  sb6rf  1782  nfsbt  1899  dvelimALT  1935  dvelimfv  1936  dvelimor  1943  eu2  1993  2euex  2036  eqcomd  2094  3eltr3g  2173  abbid  2205  neneqd  2277  syl5eqner  2287  3netr3g  2290  necomd  2342  r19.21bi  2462  nrexdv  2467  rexlimd  2487  rabbidva  2608  elisset  2634  euind  2803  rmoan  2816  reuind  2821  2rmorex  2822  spsbc  2852  spesbc  2925  eldifad  3011  eldifbd  3012  3sstr3g  3067  syl6sseq  3073  difindiss  3254  un00  3333  undifss  3367  ifcldcd  3430  disjpr2  3510  difprsn1  3582  diftpsn3  3584  difsnss  3589  sneqr  3610  preqr1  3618  preq12b  3620  oprcl  3652  intab  3723  riinm  3808  rintm  3827  disjiun  3846  sndisj  3847  3brtr3g  3882  trint  3957  iinexgm  3996  exmidexmid  4037  exmid01  4038  pwel  4054  exss  4063  0nelop  4084  euotd  4090  opelopabsb  4096  pwunim  4122  issod  4155  frind  4188  suctr  4257  orduniss  4261  onelini  4266  oneluni  4267  eusv2i  4290  rexxfrd  4298  rabxfrd  4304  reuhypd  4306  iunpw  4315  sucexg  4328  ordsucim  4330  ordtriexmidlem  4349  ordtri2or2exmidlem  4355  onsucelsucexmidlem  4358  ordsucunielexmid  4360  orddif  4376  suc11g  4386  onintexmid  4401  reg3exmidlemwe  4407  tfisi  4415  peano1  4422  peano2  4423  finds2  4429  omsinds  4448  brrelex12  4489  brel  4503  ssrel  4539  ssrel2  4541  ssrelrel  4551  elrel  4553  xpsspw  4563  relop  4599  dmxpm  4669  opelresi  4737  ndmima  4822  poirr2  4837  xpmlem  4865  xpimasn  4892  iotass  5010  iotacl  5016  dffun5r  5040  funeu  5053  funeu2  5054  funopg  5061  funun  5071  funinsn  5076  funtp  5080  funcnvuni  5096  funcnvres2  5102  imadiflem  5106  imadif  5107  funimaexglem  5110  fneu2  5132  fnimaeq0  5148  fnmpt  5153  fun2  5197  f00  5215  f0bi  5216  foimacnv  5284  resdif  5288  f1ococnv1  5295  fv3  5341  relelfvdm  5349  nfvres  5350  dffn5im  5363  mptfvex  5401  fvmptdf  5403  fvmptdv2  5405  fndmdif  5418  dff4im  5459  fmpt  5463  fmptd  5466  fmptdf  5469  f1oresrab  5477  fcoconst  5482  fsn  5483  ftpg  5495  fsnunf  5511  resfunexg  5532  isores1  5607  riota2df  5642  acexmidlemcase  5661  brabvv  5709  funoprabg  5758  fnovim  5767  ovmpt2df  5790  ovi3  5795  grprinvlem  5853  grprinvd  5854  grpridd  5855  elmpt2cl  5856  1stcof  5948  2ndcof  5949  fnmpt2  5986  fmpt2co  5995  fo2ndf  6006  f1o2ndf1  6007  disjxp1  6015  brtpos2  6030  reldmtpos  6032  dftpos3  6041  dftpos4  6042  tpostpos2  6044  tposf2  6047  tposf12  6048  tposfo  6050  tposf  6051  smores2  6073  tfrlem1  6087  tfrlem3-2d  6091  tfrlemisucaccv  6104  tfrlemibxssdm  6106  tfrlemibfn  6107  tfrlemi1  6111  tfrexlem  6113  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlembfn  6123  tfr1onlemaccex  6127  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllembfn  6136  tfrcllemaccex  6140  tfrcldm  6142  rdgivallem  6160  rdgisucinc  6164  frecabex  6177  frecfnom  6180  frecfcllem  6183  frecsuclem  6185  omsuc  6247  nntri2  6269  nnsucuniel  6270  nnsseleq  6276  nnm00  6302  ecexr  6311  swoer  6334  elqsn0m  6374  iinerm  6378  erinxp  6380  ecinxp  6381  eroveu  6397  eroprf  6399  mapprc  6423  mapsn  6461  ixpprc  6490  ixp0  6502  resixp  6504  elixpsn  6506  dom2lem  6543  fundmen  6577  dom0  6608  xpf1o  6614  mapxpen  6618  xpmapenlem  6619  ssenen  6621  nneneq  6627  ssfilem  6645  dif1en  6649  dif1enen  6650  fin0  6655  fin0or  6656  diffitest  6657  diffisn  6663  ac6sfi  6668  fimax2gtrilemstep  6670  fimax2gtri  6671  finexdc  6672  onunsnss  6681  unsnfidcel  6685  undifdcss  6687  undifdc  6688  fiintim  6693  fisseneq  6696  fidcenumlemr  6718  sbthlemi4  6723  sbthlemi5  6724  sbthlemi9  6728  suplubti  6749  supelti  6751  infmoti  6777  infisoti  6781  djulclb  6801  updjud  6827  0ct  6843  ctmlemr  6844  enumct  6847  finomni  6857  fodjuomnilemdc  6860  fodjuomnilemm  6862  fodjuomnilemres  6864  en2eleq  6882  exmidfodomrlemeldju  6886  exmidfodomrlemreseldju  6887  exmidfodomrlemim  6888  elni2  6934  indpi  6962  distrnqg  7007  subhalfnqq  7034  enq0sym  7052  enq0ref  7053  enq0tr  7054  nqnq0pi  7058  nnnq0lem1  7066  distrnq0  7079  elinp  7094  elnp1st2nd  7096  prltlu  7107  prnmaxl  7108  prnminu  7109  prarloc  7123  nqprm  7162  appdivnq  7183  prmuloc  7186  mullocpr  7191  distrlem4prl  7204  distrlem4pru  7205  ltexprlemm  7220  ltexprlemopl  7221  ltexprlemopu  7223  cauappcvgprlemopl  7266  cauappcvgprlemopu  7268  cauappcvgprlemdisj  7271  cauappcvgprlem2  7280  cauappcvgprlemlim  7281  caucvgprlemnkj  7286  caucvgprlemopl  7289  caucvgprlemopu  7291  caucvgprlemdisj  7294  caucvgprlemcl  7296  caucvgprlemladdfu  7297  caucvgprlemladdrl  7298  caucvgprlem2  7300  caucvgprprlemcbv  7307  caucvgprprlemval  7308  caucvgprprlemlol  7318  caucvgprprlemexbt  7326  caucvgprprlem1  7329  prsrlem1  7349  gt0srpr  7355  caucvgsrlemcl  7395  caucvgsrlembound  7400  caucvgsrlemgt1  7401  ltresr  7437  nnindnn  7489  axcaucvglemcl  7491  axcaucvglemval  7493  axcaucvglemcau  7494  axcaucvglemres  7495  nnind  8499  nn0supp  8786  nn0ge2m1nn  8794  zleloe  8858  zapne  8882  nn0lt2  8889  suprzclex  8905  zindd  8925  uzm1  9110  uzin  9112  elnn1uz2  9155  nn01to3  9163  divfnzn  9167  qapne  9185  xrltnsym2  9325  iooval2  9394  icoshftf1o  9469  fztri3or  9514  fzneuz  9576  4fvwrd4  9612  elfzo0  9654  exbtwnzlemex  9722  ioom  9733  fzfig  9898  uzsinds  9909  iseqovex  9931  iseqval  9932  iseqvalt  9934  seq3val  9935  iseqfclt  9940  seqf  9941  monoord2  9966  iseqf1olemjpcl  9985  iseqf1olemqpcl  9986  seq3f1olemqsum  9990  seq3f1o  9994  iseqdistr  10006  seq3distr  10007  expp1  10023  expcl2lemap  10028  expclzap  10041  expap0i  10048  ibcval5  10232  hashinfuni  10246  hashennnuni  10248  hashnncl  10265  resunimafz0  10297  zfz1isolemiso  10305  zfz1isolem1  10306  zfz1iso  10307  seq3shft  10333  cvg1nlemcau  10478  rexanuz  10482  resqrexlemoverl  10515  resqrexlemglsq  10516  resqrexlemsqa  10518  resqrexlemex  10519  rersqreu  10522  caubnd2  10611  maxleast  10707  fimaxre2  10719  minmax  10722  climreu  10746  iserex  10788  climcvg1nlem  10799  serf0  10802  fz1f1o  10825  isummolem3  10831  zisum  10835  fisum  10839  isumz  10842  isumss  10844  isumss2  10846  fisumsers  10849  fisumser  10851  fsumsplit  10862  isumclim2  10877  isumclim3  10878  fsum2dlemstep  10889  fsumcnv  10892  fisumcom2  10893  bcxmas  10944  isumle  10950  cvgratnnlemnexp  10979  cvgratnnlemmn  10980  cvgratz  10987  mertenslemub  10989  mertenslemi1  10990  mertenslem2  10991  mertensabs  10992  ef0lem  11011  mod2eq1n2dvds  11218  ndvdssub  11269  infssuzex  11284  infssuzcldc  11286  gcdsupex  11288  gcdsupcl  11289  bezoutlemnewy  11324  bezoutlemmain  11326  bezoutlembi  11333  bezoutlemeu  11335  bezoutlemle  11336  nn0seqcvgd  11362  eucalgf  11376  eucalginv  11377  lcmval  11384  prmind2  11441  dfphi2  11535  phiprmpw  11537  phimullem  11540  structcnvcnv  11571  setscom  11595  restid2  11722  topontopon  11780  eltg3i  11817  epttop  11851  difopn  11869  uncld  11874  bj-bdfindis  12115  bj-peano4  12123  strcollnfALT  12154  nnsf  12167  nninfalllem1  12171  nninfall  12172  nninfsellemqall  12179  exmidsbthrlem  12184  alsi1d  12196  alsi2d  12197  alsc1d  12198  alsc2d  12199
  Copyright terms: Public domain W3C validator