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

Theorem sylib 120
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 118 . 2 (𝜓𝜒)
41, 3syl 14 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylbb1  135  bicomd  139  pm5.74d  180  bitri  182  3imtr3i  198  ancomd  263  pm4.71d  385  pm4.71rd  386  imdistand  436  orcomd  681  3mix3  1112  mpjao3dan  1241  ecase23d  1284  exlimdh  1530  nexd  1547  alexnim  1582  excomim  1596  19.41  1619  nfexd  1688  sbh  1703  sbcof2  1735  sbidm  1776  sb6rf  1778  nfsbt  1895  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  eu2  1989  2euex  2032  eqcomd  2090  3eltr3g  2169  abbid  2201  neneqd  2272  syl5eqner  2282  3netr3g  2285  necomd  2337  r19.21bi  2457  nrexdv  2462  rexlimd  2482  rabbidva  2603  elisset  2627  euind  2793  rmoan  2804  reuind  2809  2rmorex  2810  spsbc  2840  spesbc  2913  eldifad  2999  eldifbd  3000  3sstr3g  3055  syl6sseq  3061  difindiss  3242  un00  3317  undifss  3350  ifcldcd  3412  disjpr2  3489  difprsn1  3559  diftpsn3  3561  difsnss  3566  sneqr  3587  preqr1  3595  preq12b  3597  oprcl  3629  intab  3700  riinm  3785  rintm  3800  sndisj  3816  3brtr3g  3851  trint  3926  iinexgm  3965  exmidexmid  4005  exmid01  4006  pwel  4019  exss  4028  0nelop  4049  euotd  4055  opelopabsb  4061  pwunim  4087  issod  4120  frind  4153  suctr  4222  orduniss  4226  onelini  4231  oneluni  4232  eusv2i  4251  rexxfrd  4259  rabxfrd  4265  reuhypd  4267  iunpw  4275  sucexg  4288  ordsucim  4290  ordtriexmidlem  4309  ordtri2or2exmidlem  4315  onsucelsucexmidlem  4318  ordsucunielexmid  4320  orddif  4336  suc11g  4346  onintexmid  4361  reg3exmidlemwe  4367  tfisi  4375  peano1  4382  peano2  4383  finds2  4389  omsinds  4408  brrelex12  4447  brel  4458  ssrel  4494  ssrel2  4496  ssrelrel  4506  elrel  4508  xpsspw  4518  relop  4554  dmxpm  4624  opelresi  4692  ndmima  4776  poirr2  4791  xpmlem  4818  xpimasn  4845  iotass  4963  iotacl  4969  dffun5r  4993  funeu  5005  funeu2  5006  funopg  5013  funun  5023  funinsn  5028  funtp  5032  funcnvuni  5048  funcnvres2  5054  imadiflem  5058  imadif  5059  funimaexglem  5062  fneu2  5084  fnimaeq0  5100  fnmpt  5105  fun2  5148  f00  5165  f0bi  5166  foimacnv  5234  resdif  5238  f1ococnv1  5245  fv3  5291  relelfvdm  5299  nfvres  5300  dffn5im  5313  mptfvex  5351  fvmptdf  5353  fvmptdv2  5355  fndmdif  5367  dff4im  5408  fmpt  5412  fmptd  5415  fmptdf  5418  f1oresrab  5426  fcoconst  5431  fsn  5432  ftpg  5444  fsnunf  5459  resfunexg  5479  isores1  5554  riota2df  5589  acexmidlemcase  5608  brabvv  5652  funoprabg  5701  fnovim  5710  ovmpt2df  5733  ovi3  5738  grprinvlem  5796  grprinvd  5797  grpridd  5798  elmpt2cl  5799  1stcof  5891  2ndcof  5892  fnmpt2  5929  fmpt2co  5938  fo2ndf  5949  f1o2ndf1  5950  brtpos2  5970  reldmtpos  5972  dftpos3  5981  dftpos4  5982  tpostpos2  5984  tposf2  5987  tposf12  5988  tposfo  5990  tposf  5991  smores2  6013  tfrlem1  6027  tfrlem3-2d  6031  tfrlemisucaccv  6044  tfrlemibxssdm  6046  tfrlemibfn  6047  tfrlemi1  6051  tfrexlem  6053  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemaccex  6067  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemaccex  6080  tfrcldm  6082  rdgivallem  6100  rdgisucinc  6104  frecabex  6117  frecfnom  6120  frecfcllem  6123  frecsuclem  6125  omsuc  6187  nntri2  6209  nnsucuniel  6210  nnsseleq  6216  nnm00  6240  ecexr  6249  swoer  6272  elqsn0m  6312  iinerm  6316  erinxp  6318  ecinxp  6319  eroveu  6335  eroprf  6337  mapprc  6361  mapsn  6399  dom2lem  6441  fundmen  6475  dom0  6506  xpf1o  6512  mapxpen  6516  xpmapenlem  6517  ssenen  6519  nneneq  6525  ssfilem  6543  dif1en  6547  dif1enen  6548  fin0  6553  fin0or  6554  diffitest  6555  diffisn  6561  ac6sfi  6566  fimax2gtrilemstep  6568  fimax2gtri  6569  finexdc  6570  onunsnss  6579  unsnfidcel  6583  undifdcss  6585  undifdc  6586  fisseneq  6592  sbthlemi4  6613  sbthlemi5  6614  sbthlemi9  6618  suplubti  6639  supelti  6641  infmoti  6667  infisoti  6671  djulclb  6691  updjud  6717  finomni  6740  fodjuomnilemdc  6743  fodjuomnilemm  6745  fodjuomnilemres  6747  en2eleq  6765  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  exmidfodomrlemim  6771  elni2  6817  indpi  6845  distrnqg  6890  subhalfnqq  6917  enq0sym  6935  enq0ref  6936  enq0tr  6937  nqnq0pi  6941  nnnq0lem1  6949  distrnq0  6962  elinp  6977  elnp1st2nd  6979  prltlu  6990  prnmaxl  6991  prnminu  6992  prarloc  7006  nqprm  7045  appdivnq  7066  prmuloc  7069  mullocpr  7074  distrlem4prl  7087  distrlem4pru  7088  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemopu  7106  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlem2  7163  cauappcvgprlemlim  7164  caucvgprlemnkj  7169  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemdisj  7177  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem2  7183  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemlol  7201  caucvgprprlemexbt  7209  caucvgprprlem1  7212  prsrlem1  7232  gt0srpr  7238  caucvgsrlemcl  7278  caucvgsrlembound  7283  caucvgsrlemgt1  7284  ltresr  7320  nnindnn  7372  axcaucvglemcl  7374  axcaucvglemval  7376  axcaucvglemcau  7377  axcaucvglemres  7378  nnind  8373  nn0supp  8658  nn0ge2m1nn  8666  zleloe  8730  zapne  8754  nn0lt2  8761  suprzclex  8777  zindd  8797  uzm1  8981  uzin  8983  elnn1uz2  9026  nn01to3  9034  divfnzn  9038  qapne  9056  xrltnsym2  9196  iooval2  9265  icoshftf1o  9340  fztri3or  9385  fzneuz  9445  4fvwrd4  9479  elfzo0  9521  exbtwnzlemex  9589  ioom  9600  fzfig  9765  uzsinds  9776  iseqovex  9787  iseqval  9788  iseqvalt  9790  iseqfclt  9794  monoord2  9810  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemqsum  9833  iseqf1o  9837  iseqdistr  9846  expivallem  9854  expival  9855  expp1  9860  expcl2lemap  9865  expclzap  9878  expap0i  9885  ibcval5  10067  hashinfuni  10081  hashennnuni  10083  hashnncl  10100  resunimafz0  10132  zfz1isolemiso  10140  zfz1isolem1  10141  zfz1iso  10142  cvg1nlemcau  10312  rexanuz  10316  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemsqa  10352  resqrexlemex  10353  rersqreu  10356  caubnd2  10445  maxleast  10541  fimaxre2  10551  minmax  10554  climreu  10578  iiserex  10619  climcvg1nlem  10628  serif0  10631  fz1f1o  10654  isummolem3  10659  zisum  10663  fisum  10665  isumz  10667  isumss  10669  mod2eq1n2dvds  10754  ndvdssub  10805  infssuzex  10820  infssuzcldc  10822  gcdsupex  10824  gcdsupcl  10825  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlembi  10869  bezoutlemeu  10871  bezoutlemle  10872  nn0seqcvgd  10898  eucalgf  10912  eucalginv  10913  lcmval  10920  prmind2  10977  dfphi2  11071  phiprmpw  11073  phimullem  11076  bj-bdfindis  11280  bj-peano4  11288  strcollnfALT  11319  nnsf  11333  nninfalllem1  11337  nninfall  11338  nninfsellemqall  11345  exmidsbthrlem  11350  alsi1d  11360  alsi2d  11361  alsc1d  11362  alsc2d  11363
  Copyright terms: Public domain W3C validator