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

Theorem sylc 61
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1 (𝜑𝜓)
sylc.2 (𝜑𝜒)
sylc.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
sylc (𝜑𝜃)

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3 (𝜑𝜓)
2 sylc.2 . . 3 (𝜑𝜒)
3 sylc.3 . . 3 (𝜓 → (𝜒𝜃))
41, 2, 3syl2im 38 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 48 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl3c  62  mpsyl  64  imp  122  2thd  173  jca  300  syl2anc  403  jc  613  annimdc  879  orandc  881  dn1dc  902  syl2an23an  1231  xordidc  1331  nfimd  1518  exlimd2  1527  elex22  2615  elex2  2616  spcimdv  2683  spcimedv  2685  rspcda  2707  spsbcd  2828  opth  4000  euotd  4017  ssorduni  4239  wetriext  4327  tfisi  4336  sotri2  4752  sotri3  4753  unielrel  4875  funmo  4947  fnfvima  5425  fliftfun  5467  fliftval  5471  riota5f  5523  riotass2  5525  grprinvlem  5726  grprinvd  5727  caofref  5763  tfrlem1  5957  tfrlem5  5963  tfrlemibxssdm  5976  tfrlemibfn  5977  tfrlemiex  5980  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemex  5996  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemex  6009  tfrcllemres  6011  tfrcl  6013  rdgisucinc  6034  frecabex  6047  frecabcl  6048  ertr  6187  qliftlem  6250  th3q  6277  f1dom2g  6303  dom3d  6321  en1  6346  xpdom3m  6378  xpf1o  6385  phplem4dom  6397  phpm  6400  phpelm  6401  findcard  6422  f1dmvrnfibi  6452  suplub2ti  6473  supelti  6474  ordiso2  6505  recexnq  6642  ltbtwnnqq  6667  addnnnq0  6701  mulnnnq0  6702  prltlu  6739  prarloclemn  6751  prarloc  6755  distrlem1prl  6834  distrlem1pru  6835  distrlem4prl  6836  distrlem4pru  6837  ltexprlemrl  6862  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprprlemml  6946  addsrpr  6984  mulsrpr  6985  axcaucvglemres  7127  lemul12a  8007  lemulge11  8011  nngt0  8131  nn0ge0  8380  nn0ge2m1nn  8415  zletric  8476  zlelttric  8477  nn0n0n1ge2b  8508  nn0ind-raph  8545  supinfneg  8764  infsupneg  8765  rpge0  8827  fz0fzelfz0  9215  fz0fzdiffz0  9218  ige2m2fzo  9284  elfzodifsumelfzo  9287  elfzom1elp1fzo  9288  exfzdc  9326  qletric  9330  qlelttric  9331  rebtwn2zlemshrink  9340  apbtwnz  9356  frecuzrdgtcl  9494  frecuzrdg0  9495  frecuzrdgfunlem  9501  frecuzrdg0t  9504  frecuzrdgsuctlem  9505  frecfzennn  9508  iseqovex  9529  monoord  9551  monoord2  9552  expcl2lemap  9585  leexp1a  9628  expnbnd  9693  faclbnd  9765  faclbnd6  9768  facavg  9770  sizeeqf1oi  9812  sizef1rn  9813  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemdecn  10036  resqrexlemgt0  10044  resqrexlemoverl  10045  resqrexlemglsq  10046  qabsor  10099  cau3lem  10138  climi  10264  climcn1  10285  climcn2  10286  sumeq2d  10334  sumeq2  10335  dvdsleabs2  10391  4dvdseven  10461  gcdmndc  10484  zsupcllemstep  10485  infssuzex  10489  gcdsupex  10493  gcdsupcl  10494  gcdeq0  10512  gcdaddm  10519  bezoutlemmain  10531  rppwr  10561  ialgfx  10578  eucialgcvga  10584  lcmmndc  10588  lcmval  10589  lcmcllem  10593  lcmledvds  10596  lcmeq0  10597  qredeq  10622  isprm3  10644  prmind2  10646  rpexp  10676  sqpweven  10697  2sqpwodd  10698  sumdc2  10760
  Copyright terms: Public domain W3C validator