ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylib GIF 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 (𝜑𝜓)
sylib.2 (𝜓𝜒)
Assertion
Ref Expression
sylib (𝜑𝜒)

Proof of Theorem sylib
StepHypRef Expression
1 sylib.1 . 2 (𝜑𝜓)
2 sylib.2 . . 3 (𝜓𝜒)
32biimpi 119 . 2 (𝜓𝜒)
41, 3syl 14 1 (𝜑𝜒)
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  718  3mix3  1152  mpjao3dan  1285  ecase23d  1328  exlimdh  1575  nexd  1592  alexnim  1627  excomim  1641  19.41  1664  equcomd  1683  nfexd  1734  sbh  1749  sbcof2  1782  sbidm  1823  sb6rf  1825  nfsbt  1949  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  eu2  2043  2euex  2086  eqcomd  2145  3eltr3g  2224  abbid  2256  neneqd  2329  eqnetrrid  2339  3netr3g  2342  necomd  2394  r19.21bi  2520  nrexdv  2525  rexlimd  2546  rabbidva  2674  elisset  2700  euind  2871  rmoan  2884  reuind  2889  2rmorex  2890  spsbc  2920  spesbc  2994  eldifad  3082  eldifbd  3083  3sstr3g  3139  sseqtrdi  3145  difindiss  3330  un00  3409  undifss  3443  ifcldcd  3507  disjpr2  3587  difprsn1  3659  diftpsn3  3661  difsnss  3666  sneqr  3687  preqr1  3695  preq12b  3697  oprcl  3729  intab  3800  riinm  3885  rintm  3905  disjiun  3924  sndisj  3925  3brtr3g  3961  trint  4041  iinexgm  4079  exmidexmid  4120  exmid01  4121  pwntru  4122  pwel  4140  exss  4149  0nelop  4170  euotd  4176  opelopabsb  4182  pwunim  4208  issod  4241  frind  4274  suctr  4343  orduniss  4347  onelini  4352  oneluni  4353  eusv2i  4376  rexxfrd  4384  rabxfrd  4390  reuhypd  4392  iunpw  4401  sucexg  4414  ordsucim  4416  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsucunielexmid  4446  orddif  4462  suc11g  4472  onintexmid  4487  reg3exmidlemwe  4493  tfisi  4501  peano1  4508  peano2  4509  finds2  4515  omsinds  4535  brrelex12  4577  brel  4591  ssrel  4627  ssrel2  4629  ssrelrel  4639  elrel  4641  xpsspw  4651  relop  4689  dmxpm  4759  opelresi  4830  ndmima  4916  poirr2  4931  xpmlem  4959  xpimasn  4987  iotass  5105  iotacl  5111  dffun5r  5135  funeu  5148  funeu2  5149  funfnd  5154  funopg  5157  funun  5167  funinsn  5172  funtp  5176  funcnvuni  5192  funcnvres2  5198  imadiflem  5202  imadif  5203  funimaexglem  5206  fneu2  5228  fnimaeq0  5244  fnmpt  5249  fun2  5296  f00  5314  f0bi  5315  foimacnv  5385  resdif  5389  f1ococnv1  5396  fv3  5444  relelfvdm  5453  nfvres  5454  dffn5im  5467  mptfvex  5506  fvmptdf  5508  fvmptdv2  5510  fndmdif  5525  dff4im  5566  fmpt  5570  fmptd  5574  fmptdf  5577  f1oresrab  5585  fcoconst  5591  fsn  5592  ftpg  5604  fsnunf  5620  resfunexg  5641  isores1  5715  riota2df  5750  acexmidlemcase  5769  brabvv  5817  funoprabg  5870  fnovim  5879  ovmpodf  5902  ovi3  5907  grprinvlem  5965  grprinvd  5966  grpridd  5967  elmpocl  5968  1stcof  6061  2ndcof  6062  fnmpo  6100  fmpoco  6113  fo2ndf  6124  f1o2ndf1  6125  disjxp1  6133  brtpos2  6148  reldmtpos  6150  dftpos3  6159  dftpos4  6160  tpostpos2  6162  tposf2  6165  tposf12  6166  tposfo  6168  tposf  6169  smores2  6191  tfrlem1  6205  tfrlem3-2d  6209  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi1  6229  tfrexlem  6231  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcldm  6260  rdgivallem  6278  rdgisucinc  6282  frecabex  6295  frecfnom  6298  frecfcllem  6301  frecsuclem  6303  omsuc  6368  nntri2  6390  nnsucuniel  6391  nnsseleq  6397  nnm00  6425  ecexr  6434  swoer  6457  elqsn0m  6497  iinerm  6501  erinxp  6503  ecinxp  6504  eroveu  6520  eroprf  6522  mapprc  6546  mapsn  6584  ixpprc  6613  ixp0  6625  resixp  6627  elixpsn  6629  dom2lem  6666  fundmen  6700  dom0  6732  xpf1o  6738  mapxpen  6742  xpmapenlem  6743  ssenen  6745  nneneq  6751  ssfilem  6769  dif1en  6773  dif1enen  6774  fin0  6779  fin0or  6780  diffitest  6781  diffisn  6787  ac6sfi  6792  fimax2gtrilemstep  6794  fimax2gtri  6795  finexdc  6796  onunsnss  6805  unsnfidcel  6809  undifdcss  6811  undifdc  6812  fiintim  6817  fisseneq  6820  fidcenumlemr  6843  sbthlemi4  6848  sbthlemi5  6849  sbthlemi9  6853  fifo  6868  suplubti  6887  supelti  6889  infmoti  6915  infisoti  6919  djulclb  6940  updjud  6967  omp1eomlem  6979  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumct  7000  finomni  7012  fodjuomnilemdc  7016  fodjum  7018  fodjuomnilemres  7020  fodjumkvlemres  7033  omniwomnimkv  7039  exmidonfinlem  7054  en2eleq  7056  exmidfodomrlemeldju  7060  exmidfodomrlemreseldju  7061  exmidfodomrlemim  7062  acfun  7068  exmidaclem  7069  ccfunen  7084  cc1  7085  cc2lem  7086  cc2  7087  cc3  7088  elni2  7134  indpi  7162  distrnqg  7207  subhalfnqq  7234  enq0sym  7252  enq0ref  7253  enq0tr  7254  nqnq0pi  7258  nnnq0lem1  7266  distrnq0  7279  elinp  7294  elnp1st2nd  7296  prltlu  7307  prnmaxl  7308  prnminu  7309  prarloc  7323  nqprm  7362  appdivnq  7383  prmuloc  7386  mullocpr  7391  distrlem4prl  7404  distrlem4pru  7405  ltexprlemm  7420  ltexprlemopl  7421  ltexprlemopu  7423  cauappcvgprlemopl  7466  cauappcvgprlemopu  7468  cauappcvgprlemdisj  7471  cauappcvgprlem2  7480  cauappcvgprlemlim  7481  caucvgprlemnkj  7486  caucvgprlemopl  7489  caucvgprlemopu  7491  caucvgprlemdisj  7494  caucvgprlemcl  7496  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  caucvgprlem2  7500  caucvgprprlemcbv  7507  caucvgprprlemval  7508  caucvgprprlemlol  7518  caucvgprprlemexbt  7526  caucvgprprlem1  7529  suplocexprlemrl  7537  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  suplocexprlemlub  7544  prsrlem1  7562  gt0srpr  7568  caucvgsrlemcl  7609  caucvgsrlembound  7614  caucvgsrlemgt1  7615  suplocsrlemb  7626  suplocsrlem  7628  suplocsr  7629  ltresr  7659  nnindnn  7713  axcaucvglemcl  7715  axcaucvglemval  7717  axcaucvglemcau  7718  axcaucvglemres  7719  axpre-suploclemres  7721  axpre-suploc  7722  sup3exmid  8727  nnind  8748  nn0supp  9041  nn0ge2m1nn  9049  zleloe  9113  zapne  9137  nn0lt2  9144  suprzclex  9161  zindd  9181  uzm1  9368  uzin  9370  elnn1uz2  9413  nn01to3  9421  divfnzn  9425  qapne  9443  xrltnsym2  9592  xaddass  9664  xleadd1a  9668  xlt2add  9675  xlesubadd  9678  iooval2  9710  icoshftf1o  9786  fztri3or  9831  fzneuz  9893  4fvwrd4  9929  elfzo0  9971  exbtwnzlemex  10039  ioom  10050  fzfig  10215  uzennn  10221  uzsinds  10227  iseqovex  10241  seq3val  10243  seqvalcd  10244  seqf  10246  seqovcd  10248  monoord2  10262  iseqf1olemjpcl  10280  iseqf1olemqpcl  10281  seq3f1olemqsum  10285  seq3f1o  10289  seq3distr  10298  expp1  10312  expcl2lemap  10317  expclzap  10330  expap0i  10337  bcval5  10521  hashinfuni  10535  hashennnuni  10537  hashnncl  10554  resunimafz0  10586  zfz1isolemiso  10594  zfz1isolem1  10595  zfz1iso  10596  seq3shft  10622  cvg1nlemcau  10768  rexanuz  10772  resqrexlemoverl  10805  resqrexlemglsq  10806  resqrexlemsqa  10808  resqrexlemex  10809  rersqreu  10812  caubnd2  10901  maxleast  10997  fimaxre2  11010  minmax  11013  xrmaxiflemcl  11026  xrmaxiflemab  11028  xrmaxiflemlub  11029  xrmaxadd  11042  xrminmax  11046  xrbdtri  11057  climreu  11078  reccn2ap  11094  iserex  11120  climcvg1nlem  11130  serf0  11133  fz1f1o  11156  summodclem3  11161  zsumdc  11165  fsum3  11168  isumz  11170  isumss  11172  isumss2  11174  fsumsersdc  11176  fsum3ser  11178  fsumsplit  11188  isumclim2  11203  isumclim3  11204  fsum2dlemstep  11215  fsumcnv  11218  fisumcom2  11219  bcxmas  11270  isumle  11276  cvgratnnlemnexp  11305  cvgratnnlemmn  11306  cvgratz  11313  mertenslemub  11315  mertenslemi1  11316  mertenslem2  11317  mertensabs  11318  ef0lem  11378  mod2eq1n2dvds  11587  ndvdssub  11638  infssuzex  11653  infssuzcldc  11655  gcdsupex  11657  gcdsupcl  11658  bezoutlemnewy  11695  bezoutlemmain  11697  bezoutlembi  11704  bezoutlemeu  11706  bezoutlemle  11707  nn0seqcvgd  11733  eucalgf  11747  eucalginv  11748  lcmval  11755  prmind2  11812  dfphi2  11907  phiprmpw  11909  phimullem  11912  ennnfonelemom  11932  ennnfoneleminc  11935  ennnfonelemhf1o  11937  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemdm  11944  ennnfonelemr  11947  ennnfonelemim  11948  exmidunben  11950  ctinfom  11952  inffinp1  11953  ctinf  11954  enctlem  11956  ctiunctlemu1st  11958  ctiunctlemu2nd  11959  ctiunctlemudc  11961  ctiunct  11964  ctiunctal  11965  unct  11966  structcnvcnv  11989  setscom  12013  restid2  12143  topontopon  12201  eltg3i  12239  epttop  12273  difopn  12291  uncld  12296  0nnei  12336  resttopon  12354  restabs  12358  restopnb  12364  lmcvg  12400  cnptopco  12405  cnss1  12409  cnss2  12410  cncnpi  12411  cncnp2m  12414  cnrest  12418  cnrest2  12419  cnrest2r  12420  cnptoprest  12422  cnptoprest2  12423  lmss  12429  lmff  12432  lmtopcnp  12433  lmcn  12434  txbasval  12450  upxp  12455  txcnmpt  12456  txdis1cn  12461  txlm  12462  lmcn2  12463  cnmpt11  12466  cnmpt11f  12467  cnmpt1t  12468  cnmpt12  12470  cnmpt21  12474  cnmpt21f  12475  cnmpt2t  12476  cnmpt22  12477  cnmpt22f  12478  cnmptcom  12481  hmeocnv  12490  hmeof1o  12492  hmeores  12498  txhmeo  12502  txswaphmeo  12504  isxmet2d  12531  blfvalps  12568  xblss2ps  12587  xblss2  12588  blfps  12592  blf  12593  unirnblps  12605  unirnbl  12606  isxms2  12635  bdxmet  12684  bdmet  12685  xmetxp  12690  xmettx  12693  blssioo  12728  tgioo  12729  mulcncflem  12773  dedekindeulemuub  12778  dedekindeulemub  12779  dedekindeulemloc  12780  dedekindeulemlu  12782  suplociccreex  12785  suplociccex  12786  dedekindicclemuub  12787  dedekindicclemub  12788  dedekindicclemloc  12789  dedekindicclemlu  12791  dedekindicc  12794  ivthinclemlopn  12797  ivthinclemuopn  12799  limcrcl  12810  limcmpted  12815  limccnp2lem  12828  limccnp2cntop  12829  limccoap  12830  dvrecap  12860  cosordlem  12952  bj-stand  13040  bj-bdfindis  13229  bj-peano4  13237  strcollnfALT  13268  pwtrufal  13276  pwf1oexmid  13278  exmid1stab  13279  subctctexmid  13280  pw1nct  13282  nnsf  13285  nninfalllem1  13289  nninfall  13290  nninfsellemqall  13297  exmidsbthrlem  13303  sbthom  13307  cvgcmp2nlemabs  13313  trilpo  13322  taupi  13330  alsi1d  13338  alsi2d  13339  alsc1d  13340  alsc2d  13341
  Copyright terms: Public domain W3C validator