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

Theorem syl3anc 1227
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 1166 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl111anc.4 . 2 ((𝜓𝜒𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 969
This theorem is referenced by:  syl112anc  1231  syl121anc  1232  syl211anc  1233  syl113anc  1239  syl131anc  1240  syl311anc  1241  syld3an3  1272  3jaod  1293  mpd3an23  1328  stoic4a  1419  rspc3ev  2845  sbciedf  2984  euotd  4229  ordelord  4356  wetriext  4551  releldm  4836  relelrn  4837  f1imass  5739  ovmpodxf  5961  ovmpodf  5967  fovrnd  5980  offval  6054  caoftrn  6072  offval3  6097  fnmpoovd  6177  tfrlemisucaccv  6287  tfrlemiubacc  6292  tfr1onlemsucaccv  6303  tfr1onlembfn  6306  tfrcllemsucaccv  6316  tfrcllembfn  6319  rdgss  6345  rdgisuc1  6346  rdgisucinc  6347  frecrdg  6370  mapsspm  6642  en2d  6728  en3d  6729  dom3d  6734  ssdomg  6738  f1imaen2g  6753  2dom  6765  cnven  6768  mapen  6806  mapxpen  6808  phpelm  6826  fidifsnen  6830  dif1en  6839  dif1enen  6840  diffisn  6853  isinfinf  6857  unfidisj  6881  unfiin  6885  tpfidisj  6887  xpfi  6889  fisseneq  6891  phpeqd  6892  ssfirab  6893  fnfi  6896  f1dmvrnfibi  6903  iunfidisj  6905  f1finf1o  6906  en1eqsn  6907  fidcenumlemr  6914  updjudhcoinlf  7039  updjudhcoinrg  7040  difinfinf  7060  en2eleq  7145  en2other2  7146  dju1en  7163  djuassen  7167  xpdjuen  7168  addcmpblnq  7302  addassnqg  7317  distrnqg  7322  ltsonq  7333  ltanqg  7335  ltmnqg  7336  ltaddnq  7342  ltexnqq  7343  prarloclemarch  7353  ltrnqg  7355  addcmpblnq0  7378  nnanq0  7393  distrnq0  7394  addassnq0  7397  prarloclemlt  7428  prarloclemcalc  7437  addnqprllem  7462  addnqprulem  7463  addnqprl  7464  addnqpru  7465  addlocprlemgt  7469  appdivnq  7498  prmuloclemcalc  7500  mulnqprl  7503  mulnqpru  7504  mullocprlem  7505  distrlem4prl  7519  distrlem4pru  7520  ltprordil  7524  ltexprlemopl  7536  ltexprlemopu  7538  ltexprlemloc  7542  ltexprlemru  7547  addcanprleml  7549  addcanprlemu  7550  ltaprlem  7553  ltaprg  7554  addextpr  7556  recexprlem1ssu  7569  aptipr  7576  ltmprr  7577  caucvgprlemcanl  7579  cauappcvgprlemopl  7581  cauappcvgprlemdisj  7586  cauappcvgprlemloc  7587  cauappcvgprlemladdfu  7589  cauappcvgprlemladdru  7591  cauappcvgprlemladdrl  7592  cauappcvgprlem1  7594  caucvgprlemm  7603  caucvgprlemopl  7604  caucvgprlemloc  7610  caucvgprlemladdfu  7612  caucvgprlemladdrl  7613  caucvgprprlemloccalc  7619  caucvgprprlemml  7629  caucvgprprlemopl  7632  caucvgprprlemloc  7638  caucvgprprlemexb  7642  caucvgprprlemaddq  7643  caucvgprprlem1  7644  caucvgprprlem2  7645  suplocexprlemmu  7653  suplocexprlemru  7654  addcmpblnr  7674  mulcmpblnrlemg  7675  mulcmpblnr  7676  ltsrprg  7682  distrsrg  7694  lttrsr  7697  ltsosr  7699  1idsr  7703  ltasrg  7705  recexgt0sr  7708  mulgt0sr  7713  mulextsr1lem  7715  srpospr  7718  prsradd  7721  prsrlt  7722  caucvgsrlemoffval  7731  caucvgsrlemoffgt1  7734  caucvgsrlemoffres  7735  caucvgsr  7737  ltpsrprg  7738  map2psrprg  7740  suplocsrlemb  7741  suplocsrlempr  7742  suplocsrlem  7743  pitoregt0  7784  recidpirqlemcalc  7792  axmulass  7808  axdistr  7809  rereceu  7824  recriota  7825  addassd  7915  mulassd  7916  adddid  7917  adddird  7918  lelttr  7981  letrd  8016  lelttrd  8017  lttrd  8018  mul12d  8044  mul32d  8045  mul31d  8046  add12d  8059  add32d  8060  cnegexlem3  8069  addcand  8076  addcan2d  8077  pncan  8098  pncan3  8100  subcan2  8117  subsub2  8120  subsub4  8125  npncan3  8130  pnpcan  8131  pnncan  8133  addsub4  8135  subaddd  8221  subadd2d  8222  addsubassd  8223  addsubd  8224  subadd23d  8225  addsub12d  8226  npncand  8227  nppcand  8228  nppcan2d  8229  nppcan3d  8230  subsubd  8231  subsub2d  8232  subsub3d  8233  subsub4d  8234  sub32d  8235  nnncand  8236  nnncan1d  8237  nnncan2d  8238  npncan3d  8239  pnpcand  8240  pnpcan2d  8241  pnncand  8242  ppncand  8243  subcand  8244  subcan2d  8245  subcanad  8246  subcan2ad  8248  subdid  8306  subdird  8307  ltadd2  8311  ltadd2d  8313  ltletrd  8315  ltsubadd  8324  lesubadd  8326  ltaddsub  8328  leaddsub  8330  le2add  8336  lt2add  8337  ltleadd  8338  lesub1  8348  lesub2  8349  ltsub1  8350  ltsub2  8351  lt2sub  8352  le2sub  8353  subge0  8367  lesub0  8371  ltadd1d  8430  leadd1d  8431  leadd2d  8432  ltsubaddd  8433  lesubaddd  8434  ltsubadd2d  8435  lesubadd2d  8436  ltaddsubd  8437  ltaddsub2d  8438  leaddsub2d  8439  subled  8440  lesubd  8441  ltsub23d  8442  ltsub13d  8443  lesub1d  8444  lesub2d  8445  ltsub1d  8446  ltsub2d  8447  gt0add  8465  apcotr  8499  apadd1  8500  addext  8502  mulext1  8504  mulext  8506  gtapd  8529  leltapd  8531  mulap0  8545  mul0eqap  8561  divvalap  8564  divcanap2  8570  diveqap0  8572  divrecap  8578  divassap  8580  divmulassap  8585  divmulasscomap  8586  divdirap  8587  divcanap3  8588  div11ap  8590  rec11ap  8600  divmuldivap  8602  divdivdivap  8603  divmuleqap  8607  dmdcanap  8612  ddcanap  8616  divadddivap  8617  divsubdivap  8618  redivclap  8621  apmul1  8678  divclapd  8680  divcanap1d  8681  divcanap2d  8682  divrecapd  8683  divrecap2d  8684  divcanap3d  8685  divcanap4d  8686  diveqap0d  8687  diveqap1d  8688  diveqap1ad  8689  diveqap0ad  8690  divap0bd  8692  divnegapd  8693  divneg2apd  8694  div2negapd  8695  redivclapd  8725  div2subap  8727  ltmul12a  8749  lemul12b  8750  lt2mul2div  8768  ltdiv2  8776  ltdiv23  8781  avglt1  9089  avglt2  9090  lt2halvesd  9098  div4p1lem1div2  9104  zltp1le  9239  elz2  9256  zdivmul  9275  uztrn  9476  eluzsub  9489  uz3m2nn  9505  qaddcl  9567  elpq  9580  cnref1o  9582  ltdiv2d  9650  lediv2d  9651  divlt1lt  9654  divle1le  9655  ledivge1le  9656  ltmulgt11d  9662  ltmulgt12d  9663  gt0divd  9664  ge0divd  9665  rpgecld  9666  ltmul1d  9668  ltmul2d  9669  lemul1d  9670  lemul2d  9671  ltdiv1d  9672  lediv1d  9673  ltmuldivd  9674  ltmuldiv2d  9675  lemuldivd  9676  lemuldiv2d  9677  ltdivmuld  9678  ltdivmul2d  9679  ledivmuld  9680  ledivmul2d  9681  ltdiv23d  9687  lediv23d  9688  addlelt  9698  xrltso  9726  xrlelttr  9736  xrlttrd  9739  xrlelttrd  9740  xrltletrd  9741  xrletrd  9742  xrre3  9752  xleadd1  9805  xltadd1  9806  xle2add  9809  xlt2add  9810  xlesubadd  9813  xadd4d  9815  ixxss1  9834  ixxss2  9835  ixxss12  9836  iooshf  9882  icoshftf1o  9921  ioodisj  9923  zltaddlt1le  9937  fznlem  9970  fzdifsuc  10010  fzrev  10013  fzrevral2  10035  elfz0fzfz0  10055  elfzmlbp  10061  fzctr  10062  elfzole1  10084  elfzolt2  10085  fzoss2  10101  fzospliti  10105  fzo1fzo0n0  10112  elfzo0z  10113  fzofzim  10117  fzoaddel  10121  eluzgtdifelfzo  10126  elfzodifsumelfzo  10130  ssfzo12bi  10154  elfzonelfzo  10159  fvinim0ffz  10170  rebtwn2zlemstep  10182  rebtwn2z  10184  qbtwnxr  10187  flqge  10211  2tnp1ge0ge0  10230  intfracq  10249  flqdiv  10250  modqval  10253  modqcld  10257  modqmulnn  10271  zmodcl  10273  zmodfz  10275  modqid  10278  zmodid2  10281  modqabs  10286  modqcyc  10288  modqadd1  10290  modqaddabs  10291  modqaddmod  10292  mulp1mod1  10294  modqmuladd  10295  modqmuladdim  10296  modqmuladdnn0  10297  m1modnnsub1  10299  modqltm1p1mod  10305  modqmul1  10306  modqsubmod  10311  modqsubmodmod  10312  q2txmodxeq0  10313  modaddmodup  10316  modqmulmod  10318  modqaddmulmod  10320  modqdi  10321  modqsubdir  10322  addmodlteq  10327  frecuzrdgrrn  10337  frec2uzrdg  10338  frecuzrdgrcl  10339  frecuzrdgsuc  10343  frecuzrdgrclt  10344  frecuzrdgg  10345  frecuzrdgsuctlem  10352  frecfzen2  10356  seq3val  10387  seqvalcd  10388  seqf  10390  seq3p1  10391  seqovcd  10392  seqp1cd  10395  monoord  10405  iseqf1olemqcl  10415  iseqf1olemnab  10417  iseqf1olemmo  10421  iseqf1olemqk  10423  seq3f1olemqsumkj  10427  seq3f1olemstep  10430  expnnval  10452  expnegap0  10457  rpexpcl  10468  expnegzap  10483  expgt1  10487  mulexpzap  10489  exprecap  10490  expaddzaplem  10492  expaddzap  10493  expmul  10494  expmulzap  10495  expdivap  10500  ltexp2a  10501  leexp2a  10502  leexp2r  10503  leexp1a  10504  bernneq2  10570  bernneq3  10571  expnbnd  10572  expnlbnd  10573  expnlbnd2  10574  expaddd  10584  expmuld  10585  expclzapd  10587  expap0d  10588  expnegapd  10589  exprecapd  10590  expp1zapd  10591  expm1apd  10592  sqdivapd  10595  mulexpd  10597  expge0d  10600  expge1d  10601  sqoddm1div8  10602  reexpclzapd  10607  leexp2ad  10611  facwordi  10647  faclbnd3  10650  facavg  10653  bcval  10656  bccmpl  10661  bc0k  10663  bcval5  10670  bcpasc  10673  hashfiv01gt1  10689  hashunlem  10711  hashunsng  10714  fiprsshashgt1  10724  hashdifsn  10726  hashdifpr  10727  hashfz  10728  hashxp  10733  fiubm  10735  hashfacen  10743  zfz1isolemiso  10746  zfz1isolem1  10747  zfz1iso  10748  shftfvalg  10754  seq3shft  10774  mulreap  10800  cjreb  10802  cjap  10842  cnrecnv  10846  cjdivapd  10904  redivapd  10910  imdivapd  10911  resqrexlemdecn  10948  absexpzap  11016  abslt  11024  absle  11025  elicc4abs  11030  abs3lem  11047  fzomaxdiflem  11048  cau3lem  11050  amgm2  11054  abssubge0d  11112  abssuble0d  11113  absdifltd  11114  absdifled  11115  absdivapd  11131  abs3difd  11136  qdenre  11138  maxabslemlub  11143  rexanre  11156  rexico  11157  fimaxre2  11162  lemininf  11169  ltmininf  11170  rpmincl  11173  mul0inf  11176  xrmaxiflemlub  11183  xrmaxltsup  11193  xrmaxaddlem  11195  xrmaxadd  11196  xrltmininf  11205  xrlemininf  11206  xrminltinf  11207  xrminadd  11210  xrbdtri  11211  climshftlemg  11237  climshft2  11241  addcn2  11245  mulcn2  11247  reccn2ap  11248  cn1lem  11249  climadd  11261  climmul  11262  climsub  11263  climsqz  11270  climsqz2  11271  climrecvg1n  11283  climcvg1nlem  11284  fisumss  11327  fsumsplitsn  11345  sumpr  11348  fsumsplitsnun  11354  fsum2dlemstep  11369  fisumcom2  11373  fisum0diag2  11382  fsumconst  11389  modfsummodlemstep  11392  fsumlessfi  11395  fsumabs  11400  fsumiun  11412  hashiun  11413  hash2iun  11414  hash2iun1dif1  11415  binomlem  11418  bcxmas  11424  isumshft  11425  isumlessdc  11431  expcnvap0  11437  expcnvre  11438  geosergap  11441  cvgratnnlembern  11458  cvgratnnlemnexp  11459  cvgratnnlemmn  11460  mertenslemi1  11470  fprodssdc  11525  fprodm1  11533  fprodunsn  11539  fprodeq0  11552  fprod2dlemstep  11557  fprodcom2fi  11561  fprodsplitsn  11568  fprodsplit1f  11569  efaddlem  11609  eftlub  11625  efltim  11633  eirraplem  11711  dvdsval3  11725  nndivdvds  11730  modm1div  11734  summodnegmod  11756  modmulconst  11757  dvds2subd  11761  dvds2addd  11763  dvdstrd  11764  dvdsmultr1d  11766  dvdsmultr2  11767  dvdsabseq  11779  dvdsfac  11792  dvdsmod  11794  oddge22np1  11812  ltoddhalfle  11824  halfleoddlt  11825  nn0ehalf  11834  nno  11837  nn0oddm1d2  11840  divalglemnn  11849  divalg  11855  divalgmod  11858  fldivndvdslt  11866  flodddiv4lt  11867  flodddiv4t2lthalf  11868  infssuzex  11876  dvdsbnd  11883  gcdneg  11909  gcdaddm  11911  modgcd  11918  gcdmultipled  11920  dvdsgcdidd  11921  bezoutlemnewy  11923  bezoutlemstep  11924  bezoutlembi  11932  dvdsgcdb  11940  gcdass  11942  mulgcd  11943  dvdsmulgcd  11952  rpmulgcd  11953  sqgcd  11956  nnwodc  11963  uzwodc  11964  nn0seqcvgd  11967  eucalglt  11983  gcddvdslcm  11999  lcmgcdlem  12003  lcmdvdsb  12010  lcmass  12011  ncoprmgcdne1b  12015  coprmdvds2  12019  mulgcddvds  12020  rpmulgcd2  12021  qredeu  12023  rpdvds  12025  divgcdcoprm0  12027  cncongr1  12029  cncongr2  12030  isprm2lem  12042  prmind2  12046  nprm  12049  dvdsnprmd  12051  exprmfct  12064  prmdvdsfz  12065  isprm5lem  12067  divgcdodd  12069  isprm6  12073  prmdvdsexp  12074  prmexpb  12077  prmfac1  12078  rpexp  12079  rpexp12i  12081  pw2dvdseulemle  12093  sqpweven  12101  2sqpwodd  12102  divnumden  12122  numdensq  12128  nonsq  12133  hashdvds  12147  phiprmpw  12148  crth  12150  phimullem  12151  eulerthlem1  12153  eulerthlemfi  12154  eulerthlemrprm  12155  eulerthlema  12156  eulerthlemh  12157  eulerthlemth  12158  prmdiv  12161  prmdiveq  12162  prmdivdiv  12163  hashgcdlem  12164  phisum  12166  odzdvds  12171  odzphi  12172  vfermltl  12177  powm2modprm  12178  reumodprminv  12179  modprm0  12180  nnnn0modprm0  12181  modprmn0modprm0  12182  coprimeprodsq  12183  pythagtriplem4  12194  pythagtriplem19  12208  pclemub  12213  pcprendvds2  12217  pcpremul  12219  pcval  12222  pcdiv  12228  pcqdiv  12233  pcexp  12235  pcdvdsb  12245  pcidlem  12248  pcdvdstr  12252  pcgcd1  12253  pc2dvds  12255  pcprmpw2  12258  dvdsprmpweqle  12262  pcaddlem  12264  pcadd  12265  pcmpt  12267  pcmptdvds  12269  fldivp1  12272  pcfaclem  12273  pcfac  12274  pcbc  12275  oddprmdvds  12278  prmpwdvds  12279  pockthlem  12280  pockthg  12281  1arith  12291  4sqlem5  12306  4sqlem6  12307  4sqlem7  12308  4sqlem8  12309  4sqlem9  12310  4sqlem4  12316  ennnfonelemp1  12333  ennnfonelemex  12341  ennnfonelemrn  12346  ctinfom  12355  ctiunct  12367  nninfdclemcl  12375  nninfdclemp1  12377  strsetsid  12421  fvsetsid  12422  setsabsd  12427  setscom  12428  ressid2  12447  ressval2  12448  srngstrd  12510  lmodstrd  12521  ipsstrd  12529  topgrpstrd  12539  difopn  12706  uncld  12711  ntrin  12722  clsss2  12727  ntrcls0  12729  topssnei  12760  neissex  12763  restbasg  12766  tgrest  12767  resttopon  12769  restabs  12773  restopnb  12779  cnpfval  12793  cnprcl2k  12804  tgcnp  12807  iscnp4  12816  cnpnei  12817  cnptopco  12820  cncnpi  12826  cncnp  12828  cnconst2  12831  cnrest  12833  cnrest2  12834  cnrest2r  12835  cnptopresti  12836  cnptoprest  12837  cnptoprest2  12838  lmss  12844  lmtopcnp  12848  txvalex  12852  txval  12853  txbasval  12865  txcnp  12869  txcnmpt  12871  txcn  12873  txdis1cn  12876  lmcn2  12878  cnmptc  12880  cnmpt11  12881  cnmpt1t  12883  cnmpt12  12885  cnmpt21  12889  cnmpt2t  12891  cnmpt22  12892  cnmpt22f  12893  cnmptcom  12896  hmeores  12913  txhmeo  12917  psmettri  12928  xmettri  12970  metrtri  12975  xmetres2  12977  blfvalps  12983  bldisj  12999  blgt0  13000  xblss2ps  13002  xblss2  13003  blhalf  13006  blininf  13022  blssps  13025  blss  13026  blssexps  13027  blssex  13028  blin2  13030  xmeter  13034  blnei  13090  blsscls2  13091  metss2lem  13095  bdmetval  13098  bdxmet  13099  bdbl  13101  xmetxp  13105  xmetxpbl  13106  xmettxlem  13107  xmettx  13108  metcnp3  13109  metcnp  13110  metcnp2  13111  metcnpi  13113  metcnpi2  13114  metcnpi3  13115  txmetcnp  13116  metcnpd  13118  tgqioo  13145  addcncntoplem  13149  fsumcncntop  13154  mulc1cncf  13174  cncfco  13176  mulcncflem  13188  mulcncf  13189  suplociccreex  13200  suplociccex  13201  dedekindicc  13209  ivthinclemlm  13210  ivthinclemum  13211  ivthinclemlopn  13212  ivthinclemuopn  13214  ivthinclemloc  13217  ivthdec  13220  limccl  13226  ellimc3apf  13227  limcimolemlt  13231  cnplimclemle  13235  cnplimclemr  13236  limccnpcntop  13242  limccnp2lem  13243  limccnp2cntop  13244  reldvg  13246  eldvap  13249  dvbssntrcntop  13251  dvcnp2cntop  13261  dvmulxxbr  13264  dvrecap  13275  dveflem  13285  reeff1o  13292  efltlemlt  13293  sin0pilem2  13301  ptolemy  13343  sinq12gt0  13349  cxprec  13429  rpcxproot  13432  cxpmuld  13454  rpabscxpbnd  13457  rplogbval  13461  rplogbchbase  13466  relogbval  13467  relogbzcl  13468  rplogbreexp  13469  rprelogbmul  13471  rprelogbdiv  13473  nnlogbexp  13475  relogbcxpbap  13481  logbgt0b  13482  logbgcd1irr  13483  logbgcd1irraplemexp  13484  logbgcd1irraplemap  13485  logbprmirr  13488  apdifflemr  13819  apdiff  13820  iswomni0  13823
  Copyright terms: Public domain W3C validator