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

Theorem syl3anc 1170
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 1119 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl111anc.4 . 2 ((𝜓𝜒𝜃) → 𝜏)
64, 5syl 14 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
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 922
This theorem is referenced by:  syl112anc  1174  syl121anc  1175  syl211anc  1176  syl113anc  1182  syl131anc  1183  syl311anc  1184  syld3an3  1215  3jaod  1236  mpd3an23  1271  stoic4a  1362  rspc3ev  2718  sbciedf  2850  euotd  4017  ordelord  4144  wetriext  4327  releldm  4597  relelrn  4598  f1imass  5445  ovmpt2dxf  5657  ovmpt2df  5663  fovrnd  5676  offval  5750  fnofval  5752  caoftrn  5767  offval3  5792  tfrlemisucaccv  5974  tfrlemiubacc  5979  tfr1onlemsucaccv  5990  tfr1onlembfn  5993  tfrcllemsucaccv  6003  tfrcllembfn  6006  rdgss  6032  rdgisuc1  6033  rdgisucinc  6034  frecrdg  6057  en2d  6315  en3d  6316  dom3d  6321  ssdomg  6325  f1imaen2g  6340  2dom  6352  cnven  6355  phpelm  6401  fidifsnen  6405  fidifsnid  6406  dif1en  6414  diffisn  6427  unfidisj  6442  unfiin  6444  fnfi  6446  f1dmvrnfibi  6452  en2eleq  6521  en2other2  6522  addcmpblnq  6619  addassnqg  6634  distrnqg  6639  ltsonq  6650  ltanqg  6652  ltmnqg  6653  ltaddnq  6659  ltexnqq  6660  prarloclemarch  6670  ltrnqg  6672  addcmpblnq0  6695  nnanq0  6710  distrnq0  6711  addassnq0  6714  prarloclemlt  6745  prarloclemcalc  6754  addnqprllem  6779  addnqprulem  6780  addnqprl  6781  addnqpru  6782  addlocprlemgt  6786  appdivnq  6815  prmuloclemcalc  6817  mulnqprl  6820  mulnqpru  6821  mullocprlem  6822  distrlem4prl  6836  distrlem4pru  6837  ltprordil  6841  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemloc  6859  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  ltaprlem  6870  ltaprg  6871  addextpr  6873  recexprlem1ssu  6886  aptipr  6893  ltmprr  6894  caucvgprlemcanl  6896  cauappcvgprlemopl  6898  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprprlemloccalc  6936  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemloc  6955  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  ltsrprg  6986  distrsrg  6998  lttrsr  7001  ltsosr  7003  1idsr  7007  ltasrg  7009  recexgt0sr  7012  mulgt0sr  7016  mulextsr1lem  7018  srpospr  7021  prsradd  7024  prsrlt  7025  caucvgsrlemoffval  7034  caucvgsrlemoffgt1  7037  caucvgsrlemoffres  7038  caucvgsr  7040  pitoregt0  7079  recidpirqlemcalc  7087  axmulass  7101  axdistr  7102  rereceu  7117  recriota  7118  addassd  7203  mulassd  7204  adddid  7205  adddird  7206  lelttr  7266  letrd  7300  lelttrd  7301  lttrd  7302  mul12d  7327  mul32d  7328  mul31d  7329  add12d  7342  add32d  7343  cnegexlem3  7352  addcand  7359  addcan2d  7360  pncan  7381  pncan3  7383  subcan2  7400  subsub2  7403  subsub4  7408  npncan3  7413  pnpcan  7414  pnncan  7416  addsub4  7418  subaddd  7504  subadd2d  7505  addsubassd  7506  addsubd  7507  subadd23d  7508  addsub12d  7509  npncand  7510  nppcand  7511  nppcan2d  7512  nppcan3d  7513  subsubd  7514  subsub2d  7515  subsub3d  7516  subsub4d  7517  sub32d  7518  nnncand  7519  nnncan1d  7520  nnncan2d  7521  npncan3d  7522  pnpcand  7523  pnpcan2d  7524  pnncand  7525  ppncand  7526  subcand  7527  subcan2d  7528  subcanad  7529  subcan2ad  7531  subdid  7585  subdird  7586  ltadd2  7590  ltadd2d  7592  ltletrd  7594  ltsubadd  7603  lesubadd  7605  ltaddsub  7607  leaddsub  7609  le2add  7615  lt2add  7616  ltleadd  7617  lesub1  7627  lesub2  7628  ltsub1  7629  ltsub2  7630  lt2sub  7631  le2sub  7632  subge0  7646  lesub0  7650  ltadd1d  7705  leadd1d  7706  leadd2d  7707  ltsubaddd  7708  lesubaddd  7709  ltsubadd2d  7710  lesubadd2d  7711  ltaddsubd  7712  ltaddsub2d  7713  leaddsub2d  7714  subled  7715  lesubd  7716  ltsub23d  7717  ltsub13d  7718  lesub1d  7719  lesub2d  7720  ltsub1d  7721  ltsub2d  7722  gt0add  7740  apcotr  7774  apadd1  7775  addext  7777  mulext1  7779  mulext  7781  gtapd  7802  leltapd  7804  subap0d  7807  mulap0  7811  divvalap  7829  divcanap2  7835  diveqap0  7837  divrecap  7843  divassap  7845  divmulassap  7850  divmulasscomap  7851  divdirap  7852  divcanap3  7853  div11ap  7855  rec11ap  7865  divmuldivap  7867  divdivdivap  7868  divmuleqap  7872  dmdcanap  7877  ddcanap  7881  divadddivap  7882  divsubdivap  7883  redivclap  7886  apmul1  7943  divclapd  7944  divcanap1d  7945  divcanap2d  7946  divrecapd  7947  divrecap2d  7948  divcanap3d  7949  divcanap4d  7950  diveqap0d  7951  diveqap1d  7952  diveqap1ad  7953  diveqap0ad  7954  divap0bd  7956  divnegapd  7957  divneg2apd  7958  div2negapd  7959  redivclapd  7987  ltmul12a  8005  lemul12b  8006  lt2mul2div  8024  ltdiv2  8032  ltdiv23  8037  avglt1  8336  avglt2  8337  lt2halvesd  8345  div4p1lem1div2  8351  zltp1le  8486  elz2  8500  zdivmul  8518  uztrn  8716  eluzsub  8729  uz3m2nn  8742  qaddcl  8801  cnref1o  8814  ltdiv2d  8878  lediv2d  8879  divlt1lt  8882  divle1le  8883  ledivge1le  8884  ltmulgt11d  8890  ltmulgt12d  8891  gt0divd  8892  ge0divd  8893  rpgecld  8894  ltmul1d  8896  ltmul2d  8897  lemul1d  8898  lemul2d  8899  ltdiv1d  8900  lediv1d  8901  ltmuldivd  8902  ltmuldiv2d  8903  lemuldivd  8904  lemuldiv2d  8905  ltdivmuld  8906  ltdivmul2d  8907  ledivmuld  8908  ledivmul2d  8909  ltdiv23d  8915  lediv23d  8916  addlelt  8920  xrltso  8947  xrlelttr  8952  xrlttrd  8955  xrlelttrd  8956  xrltletrd  8957  xrletrd  8958  xrre3  8965  ixxss1  9003  ixxss2  9004  ixxss12  9005  iooshf  9051  icoshftf1o  9089  ioodisj  9091  zltaddlt1le  9104  fznlem  9136  fzdifsuc  9174  fzrev  9177  fzrevral2  9199  elfz0fzfz0  9214  elfzmlbp  9220  fzctr  9221  elfzole1  9241  elfzolt2  9242  fzoss2  9258  fzospliti  9262  fzo1fzo0n0  9269  elfzo0z  9270  fzofzim  9274  fzoaddel  9278  eluzgtdifelfzo  9283  elfzodifsumelfzo  9287  ssfzo12bi  9311  elfzonelfzo  9316  fvinim0ffz  9327  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnxr  9344  flqge  9364  2tnp1ge0ge0  9383  intfracq  9402  flqdiv  9403  modqval  9406  modqcld  9410  modqmulnn  9424  zmodcl  9426  zmodfz  9428  modqid  9431  zmodid2  9434  modqabs  9439  modqcyc  9441  modqadd1  9443  modqaddabs  9444  modqaddmod  9445  mulp1mod1  9447  modqmuladd  9448  modqmuladdim  9449  modqmuladdnn0  9450  m1modnnsub1  9452  modqltm1p1mod  9458  modqmul1  9459  modqsubmod  9464  modqsubmodmod  9465  q2txmodxeq0  9466  modaddmodup  9469  modqmulmod  9471  modqaddmulmod  9473  modqdi  9474  modqsubdir  9475  addmodlteq  9480  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  frecfzen2  9509  iseqval  9530  iseqvalt  9532  iseqfclt  9536  iseqp1  9538  iseqp1t  9539  monoord  9551  expinnval  9576  expnegap0  9581  rpexpcl  9592  expnegzap  9607  expgt1  9611  mulexpzap  9613  exprecap  9614  expaddzaplem  9616  expaddzap  9617  expmul  9618  expmulzap  9619  expdivap  9624  ltexp2a  9625  leexp2a  9626  leexp2r  9627  leexp1a  9628  bernneq2  9691  bernneq3  9692  expnbnd  9693  expnlbnd  9694  expnlbnd2  9695  expaddd  9704  expmuld  9705  expclzapd  9707  expap0d  9708  expnegapd  9709  exprecapd  9710  expp1zapd  9711  expm1apd  9712  sqdivapd  9715  mulexpd  9717  expge0d  9720  expge1d  9721  sqoddm1div8  9722  reexpclzapd  9727  leexp2ad  9731  facwordi  9764  faclbnd3  9767  facavg  9770  bcval  9773  bccmpl  9778  bc0k  9780  ibcval5  9787  bcpasc  9790  sizefiv01gt1  9806  sizeunlem  9828  sizeunsng  9831  shftfvalg  9844  mulreap  9889  cjreb  9891  cjap  9931  cnrecnv  9935  cjdivapd  9993  redivapd  9999  imdivapd  10000  resqrexlemdecn  10036  absexpzap  10104  abslt  10112  absle  10113  elicc4abs  10118  abs3lem  10135  fzomaxdiflem  10136  cau3lem  10138  amgm2  10142  abssubge0d  10200  abssuble0d  10201  absdifltd  10202  absdifled  10203  absdivapd  10219  abs3difd  10224  qdenre  10226  maxabslemlub  10231  rexanre  10244  rexico  10245  fimaxre2  10247  lemininf  10253  ltmininf  10254  climshftlemg  10279  climshft2  10283  addcn2  10287  mulcn2  10289  cn1lem  10290  climadd  10302  climmul  10303  climsub  10304  climsqz  10311  climsqz2  10312  climrecvg1n  10323  climcvg1nlem  10324  dvdsval3  10344  nndivdvds  10346  summodnegmod  10371  modmulconst  10372  dvds2subd  10376  dvdsmultr1d  10379  dvdsmultr2  10380  dvdsabseq  10392  dvdsfac  10405  dvdsmod  10407  oddge22np1  10425  ltoddhalfle  10437  halfleoddlt  10438  nn0ehalf  10447  nno  10450  nn0oddm1d2  10453  divalglemnn  10462  divalg  10468  divalgmod  10471  fldivndvdslt  10479  flodddiv4lt  10480  flodddiv4t2lthalf  10481  infssuzex  10489  dvdsbnd  10492  gcdneg  10517  gcdaddm  10519  modgcd  10526  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlembi  10538  dvdsgcdb  10546  gcdass  10548  mulgcd  10549  dvdsmulgcd  10558  rpmulgcd  10559  sqgcd  10562  nn0seqcvgd  10567  eucalglt  10583  gcddvdslcm  10599  lcmgcdlem  10603  lcmdvdsb  10610  lcmass  10611  ncoprmgcdne1b  10615  coprmdvds2  10619  mulgcddvds  10620  rpmulgcd2  10621  qredeu  10623  rpdvds  10625  divgcdcoprm0  10627  cncongr1  10629  cncongr2  10630  isprm2lem  10642  prmind2  10646  nprm  10649  dvdsnprmd  10651  exprmfct  10663  prmdvdsfz  10664  divgcdodd  10666  isprm6  10670  prmdvdsexp  10671  prmexpb  10674  prmfac1  10675  rpexp  10676  rpexp12i  10678  pw2dvdseulemle  10689  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator