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

Theorem syl3anc 1216
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 1161 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl111anc.4 . 2 ((𝜓𝜒𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
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 964
This theorem is referenced by:  syl112anc  1220  syl121anc  1221  syl211anc  1222  syl113anc  1228  syl131anc  1229  syl311anc  1230  syld3an3  1261  3jaod  1282  mpd3an23  1317  stoic4a  1408  rspc3ev  2806  sbciedf  2944  euotd  4176  ordelord  4303  wetriext  4491  releldm  4774  relelrn  4775  f1imass  5675  ovmpodxf  5896  ovmpodf  5902  fovrnd  5915  offval  5989  caoftrn  6007  offval3  6032  fnmpoovd  6112  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfrcllemsucaccv  6251  tfrcllembfn  6254  rdgss  6280  rdgisuc1  6281  rdgisucinc  6282  frecrdg  6305  mapsspm  6576  en2d  6662  en3d  6663  dom3d  6668  ssdomg  6672  f1imaen2g  6687  2dom  6699  cnven  6702  mapen  6740  mapxpen  6742  phpelm  6760  fidifsnen  6764  dif1en  6773  dif1enen  6774  diffisn  6787  isinfinf  6791  unfidisj  6810  unfiin  6814  tpfidisj  6816  xpfi  6818  fisseneq  6820  phpeqd  6821  ssfirab  6822  fnfi  6825  f1dmvrnfibi  6832  iunfidisj  6834  f1finf1o  6835  en1eqsn  6836  fidcenumlemr  6843  updjudhcoinlf  6965  updjudhcoinrg  6966  difinfinf  6986  en2eleq  7056  en2other2  7057  dju1en  7074  djuassen  7078  xpdjuen  7079  addcmpblnq  7187  addassnqg  7202  distrnqg  7207  ltsonq  7218  ltanqg  7220  ltmnqg  7221  ltaddnq  7227  ltexnqq  7228  prarloclemarch  7238  ltrnqg  7240  addcmpblnq0  7263  nnanq0  7278  distrnq0  7279  addassnq0  7282  prarloclemlt  7313  prarloclemcalc  7322  addnqprllem  7347  addnqprulem  7348  addnqprl  7349  addnqpru  7350  addlocprlemgt  7354  appdivnq  7383  prmuloclemcalc  7385  mulnqprl  7388  mulnqpru  7389  mullocprlem  7390  distrlem4prl  7404  distrlem4pru  7405  ltprordil  7409  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemloc  7427  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  ltaprlem  7438  ltaprg  7439  addextpr  7441  recexprlem1ssu  7454  aptipr  7461  ltmprr  7462  caucvgprlemcanl  7464  cauappcvgprlemopl  7466  cauappcvgprlemdisj  7471  cauappcvgprlemloc  7472  cauappcvgprlemladdfu  7474  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  caucvgprlemm  7488  caucvgprlemopl  7489  caucvgprlemloc  7495  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  caucvgprprlemloccalc  7504  caucvgprprlemml  7514  caucvgprprlemopl  7517  caucvgprprlemloc  7523  caucvgprprlemexb  7527  caucvgprprlemaddq  7528  caucvgprprlem1  7529  caucvgprprlem2  7530  suplocexprlemmu  7538  suplocexprlemru  7539  addcmpblnr  7559  mulcmpblnrlemg  7560  mulcmpblnr  7561  ltsrprg  7567  distrsrg  7579  lttrsr  7582  ltsosr  7584  1idsr  7588  ltasrg  7590  recexgt0sr  7593  mulgt0sr  7598  mulextsr1lem  7600  srpospr  7603  prsradd  7606  prsrlt  7607  caucvgsrlemoffval  7616  caucvgsrlemoffgt1  7619  caucvgsrlemoffres  7620  caucvgsr  7622  ltpsrprg  7623  map2psrprg  7625  suplocsrlemb  7626  suplocsrlempr  7627  suplocsrlem  7628  pitoregt0  7669  recidpirqlemcalc  7677  axmulass  7693  axdistr  7694  rereceu  7709  recriota  7710  addassd  7800  mulassd  7801  adddid  7802  adddird  7803  lelttr  7864  letrd  7898  lelttrd  7899  lttrd  7900  mul12d  7926  mul32d  7927  mul31d  7928  add12d  7941  add32d  7942  cnegexlem3  7951  addcand  7958  addcan2d  7959  pncan  7980  pncan3  7982  subcan2  7999  subsub2  8002  subsub4  8007  npncan3  8012  pnpcan  8013  pnncan  8015  addsub4  8017  subaddd  8103  subadd2d  8104  addsubassd  8105  addsubd  8106  subadd23d  8107  addsub12d  8108  npncand  8109  nppcand  8110  nppcan2d  8111  nppcan3d  8112  subsubd  8113  subsub2d  8114  subsub3d  8115  subsub4d  8116  sub32d  8117  nnncand  8118  nnncan1d  8119  nnncan2d  8120  npncan3d  8121  pnpcand  8122  pnpcan2d  8123  pnncand  8124  ppncand  8125  subcand  8126  subcan2d  8127  subcanad  8128  subcan2ad  8130  subdid  8188  subdird  8189  ltadd2  8193  ltadd2d  8195  ltletrd  8197  ltsubadd  8206  lesubadd  8208  ltaddsub  8210  leaddsub  8212  le2add  8218  lt2add  8219  ltleadd  8220  lesub1  8230  lesub2  8231  ltsub1  8232  ltsub2  8233  lt2sub  8234  le2sub  8235  subge0  8249  lesub0  8253  ltadd1d  8312  leadd1d  8313  leadd2d  8314  ltsubaddd  8315  lesubaddd  8316  ltsubadd2d  8317  lesubadd2d  8318  ltaddsubd  8319  ltaddsub2d  8320  leaddsub2d  8321  subled  8322  lesubd  8323  ltsub23d  8324  ltsub13d  8325  lesub1d  8326  lesub2d  8327  ltsub1d  8328  ltsub2d  8329  gt0add  8347  apcotr  8381  apadd1  8382  addext  8384  mulext1  8386  mulext  8388  gtapd  8411  leltapd  8413  subap0d  8418  mulap0  8427  mul0eqap  8443  divvalap  8446  divcanap2  8452  diveqap0  8454  divrecap  8460  divassap  8462  divmulassap  8467  divmulasscomap  8468  divdirap  8469  divcanap3  8470  div11ap  8472  rec11ap  8482  divmuldivap  8484  divdivdivap  8485  divmuleqap  8489  dmdcanap  8494  ddcanap  8498  divadddivap  8499  divsubdivap  8500  redivclap  8503  apmul1  8560  divclapd  8562  divcanap1d  8563  divcanap2d  8564  divrecapd  8565  divrecap2d  8566  divcanap3d  8567  divcanap4d  8568  diveqap0d  8569  diveqap1d  8570  diveqap1ad  8571  diveqap0ad  8572  divap0bd  8574  divnegapd  8575  divneg2apd  8576  div2negapd  8577  redivclapd  8606  div2subap  8608  ltmul12a  8630  lemul12b  8631  lt2mul2div  8649  ltdiv2  8657  ltdiv23  8662  avglt1  8970  avglt2  8971  lt2halvesd  8979  div4p1lem1div2  8985  zltp1le  9120  elz2  9134  zdivmul  9153  uztrn  9354  eluzsub  9367  uz3m2nn  9380  qaddcl  9439  cnref1o  9452  ltdiv2d  9519  lediv2d  9520  divlt1lt  9523  divle1le  9524  ledivge1le  9525  ltmulgt11d  9531  ltmulgt12d  9532  gt0divd  9533  ge0divd  9534  rpgecld  9535  ltmul1d  9537  ltmul2d  9538  lemul1d  9539  lemul2d  9540  ltdiv1d  9541  lediv1d  9542  ltmuldivd  9543  ltmuldiv2d  9544  lemuldivd  9545  lemuldiv2d  9546  ltdivmuld  9547  ltdivmul2d  9548  ledivmuld  9549  ledivmul2d  9550  ltdiv23d  9556  lediv23d  9557  addlelt  9567  xrltso  9594  xrlelttr  9601  xrlttrd  9604  xrlelttrd  9605  xrltletrd  9606  xrletrd  9607  xrre3  9617  xleadd1  9670  xltadd1  9671  xle2add  9674  xlt2add  9675  xlesubadd  9678  xadd4d  9680  ixxss1  9699  ixxss2  9700  ixxss12  9701  iooshf  9747  icoshftf1o  9786  ioodisj  9788  zltaddlt1le  9801  fznlem  9833  fzdifsuc  9873  fzrev  9876  fzrevral2  9898  elfz0fzfz0  9915  elfzmlbp  9921  fzctr  9922  elfzole1  9944  elfzolt2  9945  fzoss2  9961  fzospliti  9965  fzo1fzo0n0  9972  elfzo0z  9973  fzofzim  9977  fzoaddel  9981  eluzgtdifelfzo  9986  elfzodifsumelfzo  9990  ssfzo12bi  10014  elfzonelfzo  10019  fvinim0ffz  10030  rebtwn2zlemstep  10042  rebtwn2z  10044  qbtwnxr  10047  flqge  10067  2tnp1ge0ge0  10086  intfracq  10105  flqdiv  10106  modqval  10109  modqcld  10113  modqmulnn  10127  zmodcl  10129  zmodfz  10131  modqid  10134  zmodid2  10137  modqabs  10142  modqcyc  10144  modqadd1  10146  modqaddabs  10147  modqaddmod  10148  mulp1mod1  10150  modqmuladd  10151  modqmuladdim  10152  modqmuladdnn0  10153  m1modnnsub1  10155  modqltm1p1mod  10161  modqmul1  10162  modqsubmod  10167  modqsubmodmod  10168  q2txmodxeq0  10169  modaddmodup  10172  modqmulmod  10174  modqaddmulmod  10176  modqdi  10177  modqsubdir  10178  addmodlteq  10183  frecuzrdgrrn  10193  frec2uzrdg  10194  frecuzrdgrcl  10195  frecuzrdgsuc  10199  frecuzrdgrclt  10200  frecuzrdgg  10201  frecuzrdgsuctlem  10208  frecfzen2  10212  seq3val  10243  seqvalcd  10244  seqf  10246  seq3p1  10247  seqovcd  10248  seqp1cd  10251  monoord  10261  iseqf1olemqcl  10271  iseqf1olemnab  10273  iseqf1olemmo  10277  iseqf1olemqk  10279  seq3f1olemqsumkj  10283  seq3f1olemstep  10286  expnnval  10308  expnegap0  10313  rpexpcl  10324  expnegzap  10339  expgt1  10343  mulexpzap  10345  exprecap  10346  expaddzaplem  10348  expaddzap  10349  expmul  10350  expmulzap  10351  expdivap  10356  ltexp2a  10357  leexp2a  10358  leexp2r  10359  leexp1a  10360  bernneq2  10425  bernneq3  10426  expnbnd  10427  expnlbnd  10428  expnlbnd2  10429  expaddd  10438  expmuld  10439  expclzapd  10441  expap0d  10442  expnegapd  10443  exprecapd  10444  expp1zapd  10445  expm1apd  10446  sqdivapd  10449  mulexpd  10451  expge0d  10454  expge1d  10455  sqoddm1div8  10456  reexpclzapd  10461  leexp2ad  10465  facwordi  10498  faclbnd3  10501  facavg  10504  bcval  10507  bccmpl  10512  bc0k  10514  bcval5  10521  bcpasc  10524  hashfiv01gt1  10540  hashunlem  10562  hashunsng  10565  fiprsshashgt1  10575  hashdifsn  10577  hashdifpr  10578  hashfz  10579  hashxp  10584  hashfacen  10591  zfz1isolemiso  10594  zfz1isolem1  10595  zfz1iso  10596  shftfvalg  10602  seq3shft  10622  mulreap  10648  cjreb  10650  cjap  10690  cnrecnv  10694  cjdivapd  10752  redivapd  10758  imdivapd  10759  resqrexlemdecn  10796  absexpzap  10864  abslt  10872  absle  10873  elicc4abs  10878  abs3lem  10895  fzomaxdiflem  10896  cau3lem  10898  amgm2  10902  abssubge0d  10960  abssuble0d  10961  absdifltd  10962  absdifled  10963  absdivapd  10979  abs3difd  10984  qdenre  10986  maxabslemlub  10991  rexanre  11004  rexico  11005  fimaxre2  11010  lemininf  11017  ltmininf  11018  rpmincl  11021  mul0inf  11024  xrmaxiflemlub  11029  xrmaxltsup  11039  xrmaxaddlem  11041  xrmaxadd  11042  xrltmininf  11051  xrlemininf  11052  xrminltinf  11053  xrminadd  11056  xrbdtri  11057  climshftlemg  11083  climshft2  11087  addcn2  11091  mulcn2  11093  reccn2ap  11094  cn1lem  11095  climadd  11107  climmul  11108  climsub  11109  climsqz  11116  climsqz2  11117  climrecvg1n  11129  climcvg1nlem  11130  fisumss  11173  fsumsplitsn  11191  sumpr  11194  fsumsplitsnun  11200  fsum2dlemstep  11215  fisumcom2  11219  fisum0diag2  11228  fsumconst  11235  modfsummodlemstep  11238  fsumlessfi  11241  fsumabs  11246  fsumiun  11258  hashiun  11259  hash2iun  11260  hash2iun1dif1  11261  binomlem  11264  bcxmas  11270  isumshft  11271  isumlessdc  11277  expcnvap0  11283  expcnvre  11284  geosergap  11287  cvgratnnlembern  11304  cvgratnnlemnexp  11305  cvgratnnlemmn  11306  mertenslemi1  11316  efaddlem  11392  eftlub  11408  efltim  11416  eirraplem  11494  dvdsval3  11508  nndivdvds  11510  summodnegmod  11535  modmulconst  11536  dvds2subd  11540  dvdsmultr1d  11543  dvdsmultr2  11544  dvdsabseq  11556  dvdsfac  11569  dvdsmod  11571  oddge22np1  11589  ltoddhalfle  11601  halfleoddlt  11602  nn0ehalf  11611  nno  11614  nn0oddm1d2  11617  divalglemnn  11626  divalg  11632  divalgmod  11635  fldivndvdslt  11643  flodddiv4lt  11644  flodddiv4t2lthalf  11645  infssuzex  11653  dvdsbnd  11656  gcdneg  11681  gcdaddm  11683  modgcd  11690  gcdmultipled  11692  dvdsgcdidd  11693  bezoutlemnewy  11695  bezoutlemstep  11696  bezoutlembi  11704  dvdsgcdb  11712  gcdass  11714  mulgcd  11715  dvdsmulgcd  11724  rpmulgcd  11725  sqgcd  11728  nn0seqcvgd  11733  eucalglt  11749  gcddvdslcm  11765  lcmgcdlem  11769  lcmdvdsb  11776  lcmass  11777  ncoprmgcdne1b  11781  coprmdvds2  11785  mulgcddvds  11786  rpmulgcd2  11787  qredeu  11789  rpdvds  11791  divgcdcoprm0  11793  cncongr1  11795  cncongr2  11796  isprm2lem  11808  prmind2  11812  nprm  11815  dvdsnprmd  11817  exprmfct  11829  prmdvdsfz  11830  divgcdodd  11832  isprm6  11836  prmdvdsexp  11837  prmexpb  11840  prmfac1  11841  rpexp  11842  rpexp12i  11844  pw2dvdseulemle  11856  sqpweven  11864  2sqpwodd  11865  divnumden  11885  numdensq  11891  nonsq  11896  hashdvds  11908  phiprmpw  11909  crth  11911  phimullem  11912  hashgcdlem  11914  ennnfonelemp1  11930  ennnfonelemex  11938  ennnfonelemrn  11943  ctinfom  11952  ctiunct  11964  strsetsid  12006  fvsetsid  12007  setsabsd  12012  setscom  12013  ressid2  12032  ressval2  12033  srngstrd  12095  lmodstrd  12106  ipsstrd  12114  topgrpstrd  12124  difopn  12291  uncld  12296  ntrin  12307  clsss2  12312  ntrcls0  12314  topssnei  12345  neissex  12348  restbasg  12351  tgrest  12352  resttopon  12354  restabs  12358  restopnb  12364  cnpfval  12378  cnprcl2k  12389  tgcnp  12392  iscnp4  12401  cnpnei  12402  cnptopco  12405  cncnpi  12411  cncnp  12413  cnconst2  12416  cnrest  12418  cnrest2  12419  cnrest2r  12420  cnptopresti  12421  cnptoprest  12422  cnptoprest2  12423  lmss  12429  lmtopcnp  12433  txvalex  12437  txval  12438  txbasval  12450  txcnp  12454  txcnmpt  12456  txcn  12458  txdis1cn  12461  lmcn2  12463  cnmptc  12465  cnmpt11  12466  cnmpt1t  12468  cnmpt12  12470  cnmpt21  12474  cnmpt2t  12476  cnmpt22  12477  cnmpt22f  12478  cnmptcom  12481  hmeores  12498  txhmeo  12502  psmettri  12513  xmettri  12555  metrtri  12560  xmetres2  12562  blfvalps  12568  bldisj  12584  blgt0  12585  xblss2ps  12587  xblss2  12588  blhalf  12591  blininf  12607  blssps  12610  blss  12611  blssexps  12612  blssex  12613  blin2  12615  xmeter  12619  blnei  12675  blsscls2  12676  metss2lem  12680  bdmetval  12683  bdxmet  12684  bdbl  12686  xmetxp  12690  xmetxpbl  12691  xmettxlem  12692  xmettx  12693  metcnp3  12694  metcnp  12695  metcnp2  12696  metcnpi  12698  metcnpi2  12699  metcnpi3  12700  txmetcnp  12701  metcnpd  12703  tgqioo  12730  addcncntoplem  12734  fsumcncntop  12739  mulc1cncf  12759  cncfco  12761  mulcncflem  12773  mulcncf  12774  suplociccreex  12785  suplociccex  12786  dedekindicc  12794  ivthinclemlm  12795  ivthinclemum  12796  ivthinclemlopn  12797  ivthinclemuopn  12799  ivthinclemloc  12802  ivthdec  12805  limccl  12811  ellimc3apf  12812  limcimolemlt  12816  cnplimclemle  12820  cnplimclemr  12821  limccnpcntop  12827  limccnp2lem  12828  limccnp2cntop  12829  reldvg  12831  eldvap  12834  dvbssntrcntop  12836  dvcnp2cntop  12846  dvmulxxbr  12849  dvrecap  12860  dveflem  12870  reeff1o  12877  efltlemlt  12878  sin0pilem2  12885  ptolemy  12927  sinq12gt0  12933  cxprec  13010  rpcxproot  13013  apdifflemr  13326  apdiff  13327
  Copyright terms: Public domain W3C validator