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

Theorem syl3anc 1172
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1 (𝜑𝜓)
sylXanc.2 (𝜑𝜒)
sylXanc.3 (𝜑𝜃)
syl111anc.4 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3anc (𝜑𝜏)

Proof of Theorem syl3anc
StepHypRef Expression
1 sylXanc.1 . . 3 (𝜑𝜓)
2 sylXanc.2 . . 3 (𝜑𝜒)
3 sylXanc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1121 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl111anc.4 . 2 ((𝜓𝜒𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  syl112anc  1176  syl121anc  1177  syl211anc  1178  syl113anc  1184  syl131anc  1185  syl311anc  1186  syld3an3  1217  3jaod  1238  mpd3an23  1273  stoic4a  1364  rspc3ev  2730  sbciedf  2863  euotd  4055  ordelord  4182  wetriext  4365  releldm  4638  relelrn  4639  f1imass  5514  ovmpt2dxf  5727  ovmpt2df  5733  fovrnd  5746  offval  5820  fnofval  5822  caoftrn  5837  offval3  5862  tfrlemisucaccv  6044  tfrlemiubacc  6049  tfr1onlemsucaccv  6060  tfr1onlembfn  6063  tfrcllemsucaccv  6073  tfrcllembfn  6076  rdgss  6102  rdgisuc1  6103  rdgisucinc  6104  frecrdg  6127  mapsspm  6391  en2d  6437  en3d  6438  dom3d  6443  ssdomg  6447  f1imaen2g  6462  2dom  6474  cnven  6477  mapen  6514  mapxpen  6516  phpelm  6534  fidifsnen  6538  dif1en  6547  dif1enen  6548  diffisn  6561  isinfinf  6565  unfidisj  6584  unfiin  6588  xpfi  6590  fisseneq  6592  ssfirab  6593  fnfi  6596  f1dmvrnfibi  6603  f1finf1o  6605  en1eqsn  6606  updjudhcoinlf  6715  updjudhcoinrg  6716  en2eleq  6765  en2other2  6766  addcmpblnq  6870  addassnqg  6885  distrnqg  6890  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltaddnq  6910  ltexnqq  6911  prarloclemarch  6921  ltrnqg  6923  addcmpblnq0  6946  nnanq0  6961  distrnq0  6962  addassnq0  6965  prarloclemlt  6996  prarloclemcalc  7005  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  addlocprlemgt  7037  appdivnq  7066  prmuloclemcalc  7068  mulnqprl  7071  mulnqpru  7072  mullocprlem  7073  distrlem4prl  7087  distrlem4pru  7088  ltprordil  7092  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemloc  7110  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  ltaprlem  7121  ltaprg  7122  addextpr  7124  recexprlem1ssu  7137  aptipr  7144  ltmprr  7145  caucvgprlemcanl  7147  cauappcvgprlemopl  7149  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprprlemloccalc  7187  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemloc  7206  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlem1  7212  caucvgprprlem2  7213  addcmpblnr  7229  mulcmpblnrlemg  7230  mulcmpblnr  7231  ltsrprg  7237  distrsrg  7249  lttrsr  7252  ltsosr  7254  1idsr  7258  ltasrg  7260  recexgt0sr  7263  mulgt0sr  7267  mulextsr1lem  7269  srpospr  7272  prsradd  7275  prsrlt  7276  caucvgsrlemoffval  7285  caucvgsrlemoffgt1  7288  caucvgsrlemoffres  7289  caucvgsr  7291  pitoregt0  7330  recidpirqlemcalc  7338  axmulass  7352  axdistr  7353  rereceu  7368  recriota  7369  addassd  7454  mulassd  7455  adddid  7456  adddird  7457  lelttr  7517  letrd  7551  lelttrd  7552  lttrd  7553  mul12d  7578  mul32d  7579  mul31d  7580  add12d  7593  add32d  7594  cnegexlem3  7603  addcand  7610  addcan2d  7611  pncan  7632  pncan3  7634  subcan2  7651  subsub2  7654  subsub4  7659  npncan3  7664  pnpcan  7665  pnncan  7667  addsub4  7669  subaddd  7755  subadd2d  7756  addsubassd  7757  addsubd  7758  subadd23d  7759  addsub12d  7760  npncand  7761  nppcand  7762  nppcan2d  7763  nppcan3d  7764  subsubd  7765  subsub2d  7766  subsub3d  7767  subsub4d  7768  sub32d  7769  nnncand  7770  nnncan1d  7771  nnncan2d  7772  npncan3d  7773  pnpcand  7774  pnpcan2d  7775  pnncand  7776  ppncand  7777  subcand  7778  subcan2d  7779  subcanad  7780  subcan2ad  7782  subdid  7836  subdird  7837  ltadd2  7841  ltadd2d  7843  ltletrd  7845  ltsubadd  7854  lesubadd  7856  ltaddsub  7858  leaddsub  7860  le2add  7866  lt2add  7867  ltleadd  7868  lesub1  7878  lesub2  7879  ltsub1  7880  ltsub2  7881  lt2sub  7882  le2sub  7883  subge0  7897  lesub0  7901  ltadd1d  7956  leadd1d  7957  leadd2d  7958  ltsubaddd  7959  lesubaddd  7960  ltsubadd2d  7961  lesubadd2d  7962  ltaddsubd  7963  ltaddsub2d  7964  leaddsub2d  7965  subled  7966  lesubd  7967  ltsub23d  7968  ltsub13d  7969  lesub1d  7970  lesub2d  7971  ltsub1d  7972  ltsub2d  7973  gt0add  7991  apcotr  8025  apadd1  8026  addext  8028  mulext1  8030  mulext  8032  gtapd  8053  leltapd  8055  subap0d  8058  mulap0  8062  divvalap  8080  divcanap2  8086  diveqap0  8088  divrecap  8094  divassap  8096  divmulassap  8101  divmulasscomap  8102  divdirap  8103  divcanap3  8104  div11ap  8106  rec11ap  8116  divmuldivap  8118  divdivdivap  8119  divmuleqap  8123  dmdcanap  8128  ddcanap  8132  divadddivap  8133  divsubdivap  8134  redivclap  8137  apmul1  8194  divclapd  8195  divcanap1d  8196  divcanap2d  8197  divrecapd  8198  divrecap2d  8199  divcanap3d  8200  divcanap4d  8201  diveqap0d  8202  diveqap1d  8203  diveqap1ad  8204  diveqap0ad  8205  divap0bd  8207  divnegapd  8208  divneg2apd  8209  div2negapd  8210  redivclapd  8238  ltmul12a  8256  lemul12b  8257  lt2mul2div  8275  ltdiv2  8283  ltdiv23  8288  avglt1  8587  avglt2  8588  lt2halvesd  8596  div4p1lem1div2  8602  zltp1le  8737  elz2  8751  zdivmul  8769  uztrn  8967  eluzsub  8980  uz3m2nn  8993  qaddcl  9052  cnref1o  9065  ltdiv2d  9129  lediv2d  9130  divlt1lt  9133  divle1le  9134  ledivge1le  9135  ltmulgt11d  9141  ltmulgt12d  9142  gt0divd  9143  ge0divd  9144  rpgecld  9145  ltmul1d  9147  ltmul2d  9148  lemul1d  9149  lemul2d  9150  ltdiv1d  9151  lediv1d  9152  ltmuldivd  9153  ltmuldiv2d  9154  lemuldivd  9155  lemuldiv2d  9156  ltdivmuld  9157  ltdivmul2d  9158  ledivmuld  9159  ledivmul2d  9160  ltdiv23d  9166  lediv23d  9167  addlelt  9171  xrltso  9198  xrlelttr  9203  xrlttrd  9206  xrlelttrd  9207  xrltletrd  9208  xrletrd  9209  xrre3  9216  ixxss1  9254  ixxss2  9255  ixxss12  9256  iooshf  9302  icoshftf1o  9340  ioodisj  9342  zltaddlt1le  9355  fznlem  9387  fzdifsuc  9425  fzrev  9428  fzrevral2  9450  elfz0fzfz0  9465  elfzmlbp  9471  fzctr  9472  elfzole1  9494  elfzolt2  9495  fzoss2  9511  fzospliti  9515  fzo1fzo0n0  9522  elfzo0z  9523  fzofzim  9527  fzoaddel  9531  eluzgtdifelfzo  9536  elfzodifsumelfzo  9540  ssfzo12bi  9564  elfzonelfzo  9569  fvinim0ffz  9580  rebtwn2zlemstep  9592  rebtwn2z  9594  qbtwnxr  9597  flqge  9617  2tnp1ge0ge0  9636  intfracq  9655  flqdiv  9656  modqval  9659  modqcld  9663  modqmulnn  9677  zmodcl  9679  zmodfz  9681  modqid  9684  zmodid2  9687  modqabs  9692  modqcyc  9694  modqadd1  9696  modqaddabs  9697  modqaddmod  9698  mulp1mod1  9700  modqmuladd  9701  modqmuladdim  9702  modqmuladdnn0  9703  m1modnnsub1  9705  modqltm1p1mod  9711  modqmul1  9712  modqsubmod  9717  modqsubmodmod  9718  q2txmodxeq0  9719  modaddmodup  9722  modqmulmod  9724  modqaddmulmod  9726  modqdi  9727  modqsubdir  9728  addmodlteq  9733  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgsuctlem  9758  frecfzen2  9762  iseqval  9788  iseqvalt  9790  iseqfclt  9794  iseqp1  9796  iseqp1t  9797  monoord  9809  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemmo  9825  iseqf1olemqk  9827  iseqf1olemqsumkj  9831  iseqf1olemstep  9834  expinnval  9856  expnegap0  9861  rpexpcl  9872  expnegzap  9887  expgt1  9891  mulexpzap  9893  exprecap  9894  expaddzaplem  9896  expaddzap  9897  expmul  9898  expmulzap  9899  expdivap  9904  ltexp2a  9905  leexp2a  9906  leexp2r  9907  leexp1a  9908  bernneq2  9971  bernneq3  9972  expnbnd  9973  expnlbnd  9974  expnlbnd2  9975  expaddd  9984  expmuld  9985  expclzapd  9987  expap0d  9988  expnegapd  9989  exprecapd  9990  expp1zapd  9991  expm1apd  9992  sqdivapd  9995  mulexpd  9997  expge0d  10000  expge1d  10001  sqoddm1div8  10002  reexpclzapd  10007  leexp2ad  10011  facwordi  10044  faclbnd3  10047  facavg  10050  bcval  10053  bccmpl  10058  bc0k  10060  ibcval5  10067  bcpasc  10070  hashfiv01gt1  10086  hashunlem  10108  hashunsng  10111  fiprsshashgt1  10121  hashdifsn  10123  hashdifpr  10124  hashfz  10125  hashxp  10130  hashfacen  10137  zfz1isolemiso  10140  zfz1isolem1  10141  zfz1iso  10142  shftfvalg  10148  mulreap  10193  cjreb  10195  cjap  10235  cnrecnv  10239  cjdivapd  10297  redivapd  10303  imdivapd  10304  resqrexlemdecn  10340  absexpzap  10408  abslt  10416  absle  10417  elicc4abs  10422  abs3lem  10439  fzomaxdiflem  10440  cau3lem  10442  amgm2  10446  abssubge0d  10504  abssuble0d  10505  absdifltd  10506  absdifled  10507  absdivapd  10523  abs3difd  10528  qdenre  10530  maxabslemlub  10535  rexanre  10548  rexico  10549  fimaxre2  10551  lemininf  10557  ltmininf  10558  climshftlemg  10583  climshft2  10587  addcn2  10591  mulcn2  10593  cn1lem  10594  climadd  10606  climmul  10607  climsub  10608  climsqz  10615  climsqz2  10616  climrecvg1n  10627  climcvg1nlem  10628  fisumss  10670  dvdsval3  10675  nndivdvds  10677  summodnegmod  10702  modmulconst  10703  dvds2subd  10707  dvdsmultr1d  10710  dvdsmultr2  10711  dvdsabseq  10723  dvdsfac  10736  dvdsmod  10738  oddge22np1  10756  ltoddhalfle  10768  halfleoddlt  10769  nn0ehalf  10778  nno  10781  nn0oddm1d2  10784  divalglemnn  10793  divalg  10799  divalgmod  10802  fldivndvdslt  10810  flodddiv4lt  10811  flodddiv4t2lthalf  10812  infssuzex  10820  dvdsbnd  10823  gcdneg  10848  gcdaddm  10850  modgcd  10857  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlembi  10869  dvdsgcdb  10877  gcdass  10879  mulgcd  10880  dvdsmulgcd  10889  rpmulgcd  10890  sqgcd  10893  nn0seqcvgd  10898  eucalglt  10914  gcddvdslcm  10930  lcmgcdlem  10934  lcmdvdsb  10941  lcmass  10942  ncoprmgcdne1b  10946  coprmdvds2  10950  mulgcddvds  10951  rpmulgcd2  10952  qredeu  10954  rpdvds  10956  divgcdcoprm0  10958  cncongr1  10960  cncongr2  10961  isprm2lem  10973  prmind2  10977  nprm  10980  dvdsnprmd  10982  exprmfct  10994  prmdvdsfz  10995  divgcdodd  10997  isprm6  11001  prmdvdsexp  11002  prmexpb  11005  prmfac1  11006  rpexp  11007  rpexp12i  11009  pw2dvdseulemle  11020  sqpweven  11028  2sqpwodd  11029  divnumden  11049  numdensq  11055  nonsq  11060  hashdvds  11072  phiprmpw  11073  crth  11075  phimullem  11076  hashgcdlem  11078
  Copyright terms: Public domain W3C validator