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

Theorem syl3anc 1201
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 1146 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl111anc.4 . 2 ((𝜓𝜒𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  syl112anc  1205  syl121anc  1206  syl211anc  1207  syl113anc  1213  syl131anc  1214  syl311anc  1215  syld3an3  1246  3jaod  1267  mpd3an23  1302  stoic4a  1393  rspc3ev  2780  sbciedf  2916  euotd  4146  ordelord  4273  wetriext  4461  releldm  4744  relelrn  4745  f1imass  5643  ovmpodxf  5864  ovmpodf  5870  fovrnd  5883  offval  5957  caoftrn  5975  offval3  6000  fnmpoovd  6080  tfrlemisucaccv  6190  tfrlemiubacc  6195  tfr1onlemsucaccv  6206  tfr1onlembfn  6209  tfrcllemsucaccv  6219  tfrcllembfn  6222  rdgss  6248  rdgisuc1  6249  rdgisucinc  6250  frecrdg  6273  mapsspm  6544  en2d  6630  en3d  6631  dom3d  6636  ssdomg  6640  f1imaen2g  6655  2dom  6667  cnven  6670  mapen  6708  mapxpen  6710  phpelm  6728  fidifsnen  6732  dif1en  6741  dif1enen  6742  diffisn  6755  isinfinf  6759  unfidisj  6778  unfiin  6782  tpfidisj  6784  xpfi  6786  fisseneq  6788  phpeqd  6789  ssfirab  6790  fnfi  6793  f1dmvrnfibi  6800  iunfidisj  6802  f1finf1o  6803  en1eqsn  6804  fidcenumlemr  6811  updjudhcoinlf  6933  updjudhcoinrg  6934  difinfinf  6954  en2eleq  7019  en2other2  7020  dju1en  7037  djuassen  7041  xpdjuen  7042  addcmpblnq  7143  addassnqg  7158  distrnqg  7163  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltaddnq  7183  ltexnqq  7184  prarloclemarch  7194  ltrnqg  7196  addcmpblnq0  7219  nnanq0  7234  distrnq0  7235  addassnq0  7238  prarloclemlt  7269  prarloclemcalc  7278  addnqprllem  7303  addnqprulem  7304  addnqprl  7305  addnqpru  7306  addlocprlemgt  7310  appdivnq  7339  prmuloclemcalc  7341  mulnqprl  7344  mulnqpru  7345  mullocprlem  7346  distrlem4prl  7360  distrlem4pru  7361  ltprordil  7365  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemloc  7383  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  ltaprlem  7394  ltaprg  7395  addextpr  7397  recexprlem1ssu  7410  aptipr  7417  ltmprr  7418  caucvgprlemcanl  7420  cauappcvgprlemopl  7422  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprprlemloccalc  7460  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemloc  7479  caucvgprprlemexb  7483  caucvgprprlemaddq  7484  caucvgprprlem1  7485  caucvgprprlem2  7486  suplocexprlemmu  7494  suplocexprlemru  7495  addcmpblnr  7515  mulcmpblnrlemg  7516  mulcmpblnr  7517  ltsrprg  7523  distrsrg  7535  lttrsr  7538  ltsosr  7540  1idsr  7544  ltasrg  7546  recexgt0sr  7549  mulgt0sr  7554  mulextsr1lem  7556  srpospr  7559  prsradd  7562  prsrlt  7563  caucvgsrlemoffval  7572  caucvgsrlemoffgt1  7575  caucvgsrlemoffres  7576  caucvgsr  7578  ltpsrprg  7579  map2psrprg  7581  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  pitoregt0  7625  recidpirqlemcalc  7633  axmulass  7649  axdistr  7650  rereceu  7665  recriota  7666  addassd  7756  mulassd  7757  adddid  7758  adddird  7759  lelttr  7820  letrd  7854  lelttrd  7855  lttrd  7856  mul12d  7882  mul32d  7883  mul31d  7884  add12d  7897  add32d  7898  cnegexlem3  7907  addcand  7914  addcan2d  7915  pncan  7936  pncan3  7938  subcan2  7955  subsub2  7958  subsub4  7963  npncan3  7968  pnpcan  7969  pnncan  7971  addsub4  7973  subaddd  8059  subadd2d  8060  addsubassd  8061  addsubd  8062  subadd23d  8063  addsub12d  8064  npncand  8065  nppcand  8066  nppcan2d  8067  nppcan3d  8068  subsubd  8069  subsub2d  8070  subsub3d  8071  subsub4d  8072  sub32d  8073  nnncand  8074  nnncan1d  8075  nnncan2d  8076  npncan3d  8077  pnpcand  8078  pnpcan2d  8079  pnncand  8080  ppncand  8081  subcand  8082  subcan2d  8083  subcanad  8084  subcan2ad  8086  subdid  8144  subdird  8145  ltadd2  8149  ltadd2d  8151  ltletrd  8153  ltsubadd  8162  lesubadd  8164  ltaddsub  8166  leaddsub  8168  le2add  8174  lt2add  8175  ltleadd  8176  lesub1  8186  lesub2  8187  ltsub1  8188  ltsub2  8189  lt2sub  8190  le2sub  8191  subge0  8205  lesub0  8209  ltadd1d  8267  leadd1d  8268  leadd2d  8269  ltsubaddd  8270  lesubaddd  8271  ltsubadd2d  8272  lesubadd2d  8273  ltaddsubd  8274  ltaddsub2d  8275  leaddsub2d  8276  subled  8277  lesubd  8278  ltsub23d  8279  ltsub13d  8280  lesub1d  8281  lesub2d  8282  ltsub1d  8283  ltsub2d  8284  gt0add  8302  apcotr  8336  apadd1  8337  addext  8339  mulext1  8341  mulext  8343  gtapd  8366  leltapd  8368  subap0d  8373  mulap0  8382  mul0eqap  8398  divvalap  8401  divcanap2  8407  diveqap0  8409  divrecap  8415  divassap  8417  divmulassap  8422  divmulasscomap  8423  divdirap  8424  divcanap3  8425  div11ap  8427  rec11ap  8437  divmuldivap  8439  divdivdivap  8440  divmuleqap  8444  dmdcanap  8449  ddcanap  8453  divadddivap  8454  divsubdivap  8455  redivclap  8458  apmul1  8515  divclapd  8517  divcanap1d  8518  divcanap2d  8519  divrecapd  8520  divrecap2d  8521  divcanap3d  8522  divcanap4d  8523  diveqap0d  8524  diveqap1d  8525  diveqap1ad  8526  diveqap0ad  8527  divap0bd  8529  divnegapd  8530  divneg2apd  8531  div2negapd  8532  redivclapd  8561  div2subap  8563  ltmul12a  8582  lemul12b  8583  lt2mul2div  8601  ltdiv2  8609  ltdiv23  8614  avglt1  8916  avglt2  8917  lt2halvesd  8925  div4p1lem1div2  8931  zltp1le  9066  elz2  9080  zdivmul  9099  uztrn  9298  eluzsub  9311  uz3m2nn  9324  qaddcl  9383  cnref1o  9396  ltdiv2d  9462  lediv2d  9463  divlt1lt  9466  divle1le  9467  ledivge1le  9468  ltmulgt11d  9474  ltmulgt12d  9475  gt0divd  9476  ge0divd  9477  rpgecld  9478  ltmul1d  9480  ltmul2d  9481  lemul1d  9482  lemul2d  9483  ltdiv1d  9484  lediv1d  9485  ltmuldivd  9486  ltmuldiv2d  9487  lemuldivd  9488  lemuldiv2d  9489  ltdivmuld  9490  ltdivmul2d  9491  ledivmuld  9492  ledivmul2d  9493  ltdiv23d  9499  lediv23d  9500  addlelt  9510  xrltso  9537  xrlelttr  9544  xrlttrd  9547  xrlelttrd  9548  xrltletrd  9549  xrletrd  9550  xrre3  9560  xleadd1  9613  xltadd1  9614  xle2add  9617  xlt2add  9618  xlesubadd  9621  xadd4d  9623  ixxss1  9642  ixxss2  9643  ixxss12  9644  iooshf  9690  icoshftf1o  9729  ioodisj  9731  zltaddlt1le  9744  fznlem  9776  fzdifsuc  9816  fzrev  9819  fzrevral2  9841  elfz0fzfz0  9858  elfzmlbp  9864  fzctr  9865  elfzole1  9887  elfzolt2  9888  fzoss2  9904  fzospliti  9908  fzo1fzo0n0  9915  elfzo0z  9916  fzofzim  9920  fzoaddel  9924  eluzgtdifelfzo  9929  elfzodifsumelfzo  9933  ssfzo12bi  9957  elfzonelfzo  9962  fvinim0ffz  9973  rebtwn2zlemstep  9985  rebtwn2z  9987  qbtwnxr  9990  flqge  10010  2tnp1ge0ge0  10029  intfracq  10048  flqdiv  10049  modqval  10052  modqcld  10056  modqmulnn  10070  zmodcl  10072  zmodfz  10074  modqid  10077  zmodid2  10080  modqabs  10085  modqcyc  10087  modqadd1  10089  modqaddabs  10090  modqaddmod  10091  mulp1mod1  10093  modqmuladd  10094  modqmuladdim  10095  modqmuladdnn0  10096  m1modnnsub1  10098  modqltm1p1mod  10104  modqmul1  10105  modqsubmod  10110  modqsubmodmod  10111  q2txmodxeq0  10112  modaddmodup  10115  modqmulmod  10117  modqaddmulmod  10119  modqdi  10120  modqsubdir  10121  addmodlteq  10126  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  frecfzen2  10155  seq3val  10186  seqvalcd  10187  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  monoord  10204  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemmo  10220  iseqf1olemqk  10222  seq3f1olemqsumkj  10226  seq3f1olemstep  10229  expnnval  10251  expnegap0  10256  rpexpcl  10267  expnegzap  10282  expgt1  10286  mulexpzap  10288  exprecap  10289  expaddzaplem  10291  expaddzap  10292  expmul  10293  expmulzap  10294  expdivap  10299  ltexp2a  10300  leexp2a  10301  leexp2r  10302  leexp1a  10303  bernneq2  10368  bernneq3  10369  expnbnd  10370  expnlbnd  10371  expnlbnd2  10372  expaddd  10381  expmuld  10382  expclzapd  10384  expap0d  10385  expnegapd  10386  exprecapd  10387  expp1zapd  10388  expm1apd  10389  sqdivapd  10392  mulexpd  10394  expge0d  10397  expge1d  10398  sqoddm1div8  10399  reexpclzapd  10404  leexp2ad  10408  facwordi  10441  faclbnd3  10444  facavg  10447  bcval  10450  bccmpl  10455  bc0k  10457  bcval5  10464  bcpasc  10467  hashfiv01gt1  10483  hashunlem  10505  hashunsng  10508  fiprsshashgt1  10518  hashdifsn  10520  hashdifpr  10521  hashfz  10522  hashxp  10527  hashfacen  10534  zfz1isolemiso  10537  zfz1isolem1  10538  zfz1iso  10539  shftfvalg  10545  seq3shft  10565  mulreap  10591  cjreb  10593  cjap  10633  cnrecnv  10637  cjdivapd  10695  redivapd  10701  imdivapd  10702  resqrexlemdecn  10739  absexpzap  10807  abslt  10815  absle  10816  elicc4abs  10821  abs3lem  10838  fzomaxdiflem  10839  cau3lem  10841  amgm2  10845  abssubge0d  10903  abssuble0d  10904  absdifltd  10905  absdifled  10906  absdivapd  10922  abs3difd  10927  qdenre  10929  maxabslemlub  10934  rexanre  10947  rexico  10948  fimaxre2  10953  lemininf  10960  ltmininf  10961  rpmincl  10964  mul0inf  10967  xrmaxiflemlub  10972  xrmaxltsup  10982  xrmaxaddlem  10984  xrmaxadd  10985  xrltmininf  10994  xrlemininf  10995  xrminltinf  10996  xrminadd  10999  xrbdtri  11000  climshftlemg  11026  climshft2  11030  addcn2  11034  mulcn2  11036  reccn2ap  11037  cn1lem  11038  climadd  11050  climmul  11051  climsub  11052  climsqz  11059  climsqz2  11060  climrecvg1n  11072  climcvg1nlem  11073  fisumss  11116  fsumsplitsn  11134  sumpr  11137  fsumsplitsnun  11143  fsum2dlemstep  11158  fisumcom2  11162  fisum0diag2  11171  fsumconst  11178  modfsummodlemstep  11181  fsumlessfi  11184  fsumabs  11189  fsumiun  11201  hashiun  11202  hash2iun  11203  hash2iun1dif1  11204  binomlem  11207  bcxmas  11213  isumshft  11214  isumlessdc  11220  expcnvap0  11226  expcnvre  11227  geosergap  11230  cvgratnnlembern  11247  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  mertenslemi1  11259  efaddlem  11294  eftlub  11310  efltim  11318  eirraplem  11395  dvdsval3  11409  nndivdvds  11411  summodnegmod  11436  modmulconst  11437  dvds2subd  11441  dvdsmultr1d  11444  dvdsmultr2  11445  dvdsabseq  11457  dvdsfac  11470  dvdsmod  11472  oddge22np1  11490  ltoddhalfle  11502  halfleoddlt  11503  nn0ehalf  11512  nno  11515  nn0oddm1d2  11518  divalglemnn  11527  divalg  11533  divalgmod  11536  fldivndvdslt  11544  flodddiv4lt  11545  flodddiv4t2lthalf  11546  infssuzex  11554  dvdsbnd  11557  gcdneg  11582  gcdaddm  11584  modgcd  11591  gcdmultipled  11593  dvdsgcdidd  11594  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlembi  11605  dvdsgcdb  11613  gcdass  11615  mulgcd  11616  dvdsmulgcd  11625  rpmulgcd  11626  sqgcd  11629  nn0seqcvgd  11634  eucalglt  11650  gcddvdslcm  11666  lcmgcdlem  11670  lcmdvdsb  11677  lcmass  11678  ncoprmgcdne1b  11682  coprmdvds2  11686  mulgcddvds  11687  rpmulgcd2  11688  qredeu  11690  rpdvds  11692  divgcdcoprm0  11694  cncongr1  11696  cncongr2  11697  isprm2lem  11709  prmind2  11713  nprm  11716  dvdsnprmd  11718  exprmfct  11730  prmdvdsfz  11731  divgcdodd  11733  isprm6  11737  prmdvdsexp  11738  prmexpb  11741  prmfac1  11742  rpexp  11743  rpexp12i  11745  pw2dvdseulemle  11756  sqpweven  11764  2sqpwodd  11765  divnumden  11785  numdensq  11791  nonsq  11796  hashdvds  11808  phiprmpw  11809  crth  11811  phimullem  11812  hashgcdlem  11814  ennnfonelemp1  11830  ennnfonelemex  11838  ennnfonelemrn  11843  ctinfom  11852  ctiunct  11864  strsetsid  11903  fvsetsid  11904  setsabsd  11909  setscom  11910  ressid2  11929  ressval2  11930  srngstrd  11992  lmodstrd  12003  ipsstrd  12011  topgrpstrd  12021  difopn  12188  uncld  12193  ntrin  12204  clsss2  12209  ntrcls0  12211  topssnei  12242  neissex  12245  restbasg  12248  tgrest  12249  resttopon  12251  restabs  12255  restopnb  12261  cnpfval  12275  cnprcl2k  12286  tgcnp  12289  iscnp4  12298  cnpnei  12299  cnptopco  12302  cncnpi  12308  cncnp  12310  cnconst2  12313  cnrest  12315  cnrest2  12316  cnrest2r  12317  cnptopresti  12318  cnptoprest  12319  cnptoprest2  12320  lmss  12326  lmtopcnp  12330  txvalex  12334  txval  12335  txbasval  12347  txcnp  12351  txcnmpt  12353  txcn  12355  txdis1cn  12358  lmcn2  12360  cnmptc  12362  cnmpt11  12363  cnmpt1t  12365  cnmpt12  12367  cnmpt21  12371  cnmpt2t  12373  cnmpt22  12374  cnmpt22f  12375  cnmptcom  12378  hmeores  12395  txhmeo  12399  psmettri  12410  xmettri  12452  metrtri  12457  xmetres2  12459  blfvalps  12465  bldisj  12481  blgt0  12482  xblss2ps  12484  xblss2  12485  blhalf  12488  blininf  12504  blssps  12507  blss  12508  blssexps  12509  blssex  12510  blin2  12512  xmeter  12516  blnei  12572  blsscls2  12573  metss2lem  12577  bdmetval  12580  bdxmet  12581  bdbl  12583  xmetxp  12587  xmetxpbl  12588  xmettxlem  12589  xmettx  12590  metcnp3  12591  metcnp  12592  metcnp2  12593  metcnpi  12595  metcnpi2  12596  metcnpi3  12597  txmetcnp  12598  metcnpd  12600  tgqioo  12627  addcncntoplem  12631  fsumcncntop  12636  mulc1cncf  12656  cncfco  12658  mulcncflem  12670  mulcncf  12671  suplociccreex  12682  suplociccex  12683  dedekindicc  12691  ivthinclemlm  12692  ivthinclemum  12693  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthinclemloc  12699  ivthdec  12702  limccl  12708  ellimc3apf  12709  limcimolemlt  12713  cnplimclemle  12717  cnplimclemr  12718  limccnpcntop  12724  limccnp2lem  12725  limccnp2cntop  12726  reldvg  12728  eldvap  12731  dvbssntrcntop  12733  dvcnp2cntop  12743  dvmulxxbr  12746  dvrecap  12757  dveflem  12766  sin0pilem2  12774  ptolemy  12816  sinq12gt0  12822
  Copyright terms: Public domain W3C validator