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  1110  mpjao3dan  1239  ecase23d  1282  exlimdh  1528  nexd  1545  alexnim  1580  excomim  1594  19.41  1617  nfexd  1685  sbh  1700  sbcof2  1732  sbidm  1773  sb6rf  1775  nfsbt  1892  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  eu2  1986  2euex  2029  eqcomd  2087  3eltr3g  2164  abbid  2196  neneqd  2267  syl5eqner  2277  3netr3g  2280  necomd  2332  r19.21bi  2450  nrexdv  2455  rexlimd  2475  rabbidva  2593  elisset  2614  euind  2780  rmoan  2791  reuind  2796  2rmorex  2797  spsbc  2827  spesbc  2900  eldifad  2985  eldifbd  2986  3sstr3g  3040  syl6sseq  3046  difindiss  3219  un00  3291  undifss  3324  ifcldcd  3383  disjpr2  3458  difprsn1  3527  diftpsn3  3529  difsnss  3533  sneqr  3554  preqr1  3562  preq12b  3564  oprcl  3596  intab  3667  riinm  3752  rintm  3767  sndisj  3783  3brtr3g  3818  trint  3892  iinexgm  3931  pwel  3975  exss  3984  0nelop  4005  euotd  4011  opelopabsb  4017  pwunim  4043  issod  4076  frind  4109  suctr  4178  orduniss  4182  onelini  4187  oneluni  4188  eusv2i  4207  rexxfrd  4215  rabxfrd  4221  reuhypd  4223  iunpw  4231  sucexg  4244  ordsucim  4246  ordtriexmidlem  4265  ordtri2or2exmidlem  4271  onsucelsucexmidlem  4274  ordsucunielexmid  4276  orddif  4292  suc11g  4302  onintexmid  4317  reg3exmidlemwe  4323  tfisi  4330  peano1  4337  peano2  4338  finds2  4344  brrelex12  4401  brel  4412  ssrel  4448  ssrel2  4450  ssrelrel  4460  elrel  4462  xpsspw  4472  relop  4508  dmxpm  4577  opelresi  4645  ndmima  4726  poirr2  4741  xpmlem  4768  xpimasn  4793  iotass  4908  iotacl  4914  dffun5r  4938  funeu  4950  funeu2  4951  funopg  4958  funun  4968  funinsn  4973  funtp  4977  funcnvuni  4993  funcnvres2  4999  imadiflem  5003  imadif  5004  funimaexglem  5007  fneu2  5029  fnimaeq0  5045  fnmpt  5050  fun2  5089  f00  5106  foimacnv  5169  resdif  5173  f1ococnv1  5180  fv3  5223  relelfvdm  5231  nfvres  5232  dffn5im  5245  mptfvex  5282  fvmptdf  5284  fvmptdv2  5286  fndmdif  5298  dff4im  5339  fmpt  5345  fmptd  5348  f1oresrab  5355  fcoconst  5360  fsn  5361  ftpg  5373  fsnunf  5388  resfunexg  5408  isores1  5479  riota2df  5513  acexmidlemcase  5532  brabvv  5576  funoprabg  5625  fnovim  5634  ovmpt2df  5657  ovi3  5662  grprinvlem  5720  grprinvd  5721  grpridd  5722  elmpt2cl  5723  1stcof  5815  2ndcof  5816  fnmpt2  5853  fmpt2co  5862  fo2ndf  5873  f1o2ndf1  5874  brtpos2  5894  reldmtpos  5896  dftpos3  5905  dftpos4  5906  tpostpos2  5908  tposf2  5911  tposf12  5912  tposfo  5914  tposf  5915  smores2  5937  tfrlem1  5951  tfrlem3-2d  5955  tfrlemisucaccv  5968  tfrlemibxssdm  5970  tfrlemibfn  5971  tfrlemi1  5975  tfrexlem  5977  tfr1onlemsucaccv  5984  tfr1onlembxssdm  5986  tfr1onlembfn  5987  tfr1onlemaccex  5991  tfrcllemsucaccv  5997  tfrcllembxssdm  5999  tfrcllembfn  6000  tfrcllemaccex  6004  tfrcldm  6006  rdgivallem  6024  rdgisucinc  6028  frecabex  6041  frecfnom  6044  frecfcllem  6047  frecsuclem  6049  omsuc  6109  nntri2  6131  nnsucuniel  6132  nnsseleq  6138  nndifsnid  6139  nnm00  6161  ecexr  6170  swoer  6193  elqsn0m  6233  iinerm  6237  erinxp  6239  ecinxp  6240  eroveu  6256  eroprf  6258  dom2lem  6311  fundmen  6345  xpf1o  6375  nneneq  6382  fidifsnid  6396  ssfilem  6400  dif1en  6404  fin0  6409  fin0or  6410  diffitest  6411  diffisn  6417  ac6sfi  6421  onunsnss  6427  unsnfidcel  6431  undiffi  6433  suplubti  6462  supelti  6464  infmoti  6490  infisoti  6494  en2eleq  6511  elni2  6555  indpi  6583  distrnqg  6628  subhalfnqq  6655  enq0sym  6673  enq0ref  6674  enq0tr  6675  nqnq0pi  6679  nnnq0lem1  6687  distrnq0  6700  elinp  6715  elnp1st2nd  6717  prltlu  6728  prnmaxl  6729  prnminu  6730  prarloc  6744  nqprm  6783  appdivnq  6804  prmuloc  6807  mullocpr  6812  distrlem4prl  6825  distrlem4pru  6826  ltexprlemm  6841  ltexprlemopl  6842  ltexprlemopu  6844  cauappcvgprlemopl  6887  cauappcvgprlemopu  6889  cauappcvgprlemdisj  6892  cauappcvgprlem2  6901  cauappcvgprlemlim  6902  caucvgprlemnkj  6907  caucvgprlemopl  6910  caucvgprlemopu  6912  caucvgprlemdisj  6915  caucvgprlemcl  6917  caucvgprlemladdfu  6918  caucvgprlemladdrl  6919  caucvgprlem2  6921  caucvgprprlemcbv  6928  caucvgprprlemval  6929  caucvgprprlemlol  6939  caucvgprprlemexbt  6947  caucvgprprlem1  6950  prsrlem1  6970  gt0srpr  6976  caucvgsrlemcl  7016  caucvgsrlembound  7021  caucvgsrlemgt1  7022  ltresr  7058  nnindnn  7110  axcaucvglemcl  7112  axcaucvglemval  7114  axcaucvglemcau  7115  axcaucvglemres  7116  nnind  8111  nn0supp  8396  nn0ge2m1nn  8404  zleloe  8468  zapne  8492  nn0lt2  8499  suprzclex  8515  zindd  8535  uzm1  8719  uzin  8721  elnn1uz2  8764  nn01to3  8772  divfnzn  8776  qapne  8794  xrltnsym2  8934  iooval2  9003  icoshftf1o  9078  fztri3or  9123  fzneuz  9183  4fvwrd4  9216  elfzo0  9257  exbtwnzlemex  9325  ioom  9336  fzfig  9501  uzsinds  9507  iseqovex  9518  iseqval  9519  iseqvalt  9521  iseqfclt  9525  monoord2  9541  iseqdistr  9556  expivallem  9563  expival  9564  expp1  9569  expcl2lemap  9574  expclzap  9587  expap0i  9594  ibcval5  9776  sizeinfuni  9790  sizeennnuni  9792  sizenncl  9809  cvg1nlemcau  9997  rexanuz  10001  resqrexlemoverl  10034  resqrexlemglsq  10035  resqrexlemsqa  10037  resqrexlemex  10038  rersqreu  10041  caubnd2  10130  maxleast  10226  fimaxre2  10236  minmax  10239  climreu  10263  iiserex  10304  climcvg1nlem  10313  serif0  10316  fz1f1o  10325  mod2eq1n2dvds  10412  ndvdssub  10463  infssuzex  10478  infssuzcldc  10480  gcdsupex  10482  gcdsupcl  10483  bezoutlemnewy  10518  bezoutlemmain  10520  bezoutlembi  10527  bezoutlemeu  10529  bezoutlemle  10530  nn0seqcvgd  10556  eucalgf  10570  eucalginv  10571  lcmval  10578  prmind2  10635  bj-bdfindis  10885  bj-peano4  10893  strcollnfALT  10924  alsi1d  10935  alsi2d  10936  alsc1d  10937  alsc2d  10938
  Copyright terms: Public domain W3C validator