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

Theorem syl3anc 1134
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 1083 . 2 (φ → (ψ χ θ))
5 syl111anc.4 . 2 ((ψ χ θ) → τ)
64, 5syl 14 1 (φτ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  syl112anc  1138  syl121anc  1139  syl211anc  1140  syl113anc  1146  syl131anc  1147  syl311anc  1148  syld3an3  1179  3jaod  1198  mpd3an23  1233  stoic4a  1318  rspc3ev  2660  sbciedf  2792  euotd  3982  ordelord  4084  releldm  4512  relelrn  4513  f1imass  5356  ovmpt2dxf  5568  ovmpt2df  5574  fovrnd  5587  offval  5661  fnofval  5663  caoftrn  5678  offval3  5703  tfrlemisucaccv  5880  tfrlemiubacc  5885  rdgss  5910  rdgisuc1  5911  rdgisucinc  5912  freccl  5932  en2d  6184  en3d  6185  dom3d  6190  ssdomg  6194  f1imaen2g  6209  2dom  6221  cnven  6224  addcmpblnq  6351  addassnqg  6366  distrnqg  6371  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltaddnq  6390  ltexnqq  6391  prarloclemarch  6401  ltrnqg  6403  addcmpblnq0  6426  nnanq0  6441  distrnq0  6442  addassnq0  6445  prarloclemlt  6476  prarloclemcalc  6485  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemgt  6517  appdivnq  6544  prmuloclemcalc  6546  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  ltaprlem  6591  ltaprg  6592  addextpr  6593  recexprlem1ssu  6606  aptipr  6613  ltmprr  6614  cauappcvgprlemcan  6616  cauappcvgprlemopl  6618  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  ltsrprg  6675  distrsrg  6687  lttrsr  6690  ltsosr  6692  1idsr  6696  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  mulextsr1lem  6706  axmulass  6757  axdistr  6758  addassd  6847  mulassd  6848  adddid  6849  adddird  6850  lelttr  6903  letrd  6935  lelttrd  6936  lttrd  6937  mul12d  6962  mul32d  6963  mul31d  6964  add12d  6975  add32d  6976  cnegexlem3  6985  addcand  6992  addcan2d  6993  pncan  7014  pncan3  7016  subcan2  7032  subsub2  7035  subsub4  7040  npncan3  7045  pnpcan  7046  pnncan  7048  addsub4  7050  subaddd  7136  subadd2d  7137  addsubassd  7138  addsubd  7139  subadd23d  7140  addsub12d  7141  npncand  7142  nppcand  7143  nppcan2d  7144  nppcan3d  7145  subsubd  7146  subsub2d  7147  subsub3d  7148  subsub4d  7149  sub32d  7150  nnncand  7151  nnncan1d  7152  nnncan2d  7153  npncan3d  7154  pnpcand  7155  pnpcan2d  7156  pnncand  7157  ppncand  7158  subcand  7159  subcan2d  7160  subcanad  7161  subcan2ad  7163  subdid  7207  subdird  7208  ltadd2  7212  ltadd2d  7214  ltletrd  7216  ltsubadd  7222  lesubadd  7224  ltaddsub  7226  leaddsub  7228  le2add  7234  lt2add  7235  ltleadd  7236  lesub1  7246  lesub2  7247  ltsub1  7248  ltsub2  7249  lt2sub  7250  le2sub  7251  subge0  7265  lesub0  7269  ltadd1d  7324  leadd1d  7325  leadd2d  7326  ltsubaddd  7327  lesubaddd  7328  ltsubadd2d  7329  lesubadd2d  7330  ltaddsubd  7331  ltaddsub2d  7332  leaddsub2d  7333  subled  7334  lesubd  7335  ltsub23d  7336  ltsub13d  7337  lesub1d  7338  lesub2d  7339  ltsub1d  7340  ltsub2d  7341  gt0add  7357  apcotr  7391  apadd1  7392  addext  7394  mulext1  7396  mulext  7398  mulap0  7417  divvalap  7435  divcanap2  7441  diveqap0  7443  divrecap  7449  divassap  7451  divdirap  7456  divcanap3  7457  div11ap  7459  rec11ap  7468  divmuldivap  7470  divdivdivap  7471  divmuleqap  7475  dmdcanap  7480  ddcanap  7484  divadddivap  7485  divsubdivap  7486  redivclap  7489  apmul1  7546  divclapd  7547  divcanap1d  7548  divcanap2d  7549  divrecapd  7550  divrecap2d  7551  divcanap3d  7552  divcanap4d  7553  diveqap0d  7554  diveqap1d  7555  diveqap1ad  7556  diveqap0ad  7557  divap0bd  7559  divnegapd  7560  divneg2apd  7561  div2negapd  7562  redivclapd  7589  ltmul12a  7607  lemul12b  7608  lt2mul2div  7626  ltdiv2  7634  ltdiv23  7639  avglt1  7940  avglt2  7941  lt2halvesd  7949  zltp1le  8074  elz2  8088  zdivmul  8106  uztrn  8265  eluzsub  8278  uz3m2nn  8291  qaddcl  8346  cnref1o  8357  ltdiv2d  8420  lediv2d  8421  ltmulgt11d  8428  ltmulgt12d  8429  gt0divd  8430  ge0divd  8431  rpgecld  8432  ltmul1d  8434  ltmul2d  8435  lemul1d  8436  lemul2d  8437  ltdiv1d  8438  lediv1d  8439  ltmuldivd  8440  ltmuldiv2d  8441  lemuldivd  8442  lemuldiv2d  8443  ltdivmuld  8444  ltdivmul2d  8445  ledivmuld  8446  ledivmul2d  8447  ltdiv23d  8453  lediv23d  8454  xrltso  8487  xrlelttr  8492  xrlttrd  8495  xrlelttrd  8496  xrltletrd  8497  xrletrd  8498  xrre3  8505  ixxss1  8543  ixxss2  8544  ixxss12  8545  iooshf  8591  icoshftf1o  8629  ioodisj  8631  fznlem  8675  fzdifsuc  8713  fzrev  8716  fzrevral2  8738  elfz0fzfz0  8753  elfzmlbp  8760  fzctr  8761  elfzole1  8781  elfzolt2  8782  fzoss2  8798  fzospliti  8802  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  fzoaddel  8818  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  ssfzo12bi  8851  elfzonelfzo  8856  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgsuc  8882  frecfzen2  8885  iseqval  8900  iseqp1  8904  expinnval  8912  expnegap0  8917  rpexpcl  8928  expnegzap  8943  expgt1  8947  mulexpzap  8949  exprecap  8950  expaddzaplem  8952  expaddzap  8953  expmul  8954  expmulzap  8955  expdivap  8959  ltexp2a  8960  leexp2a  8961  leexp2r  8962  leexp1a  8963  bernneq2  9023  bernneq3  9024  expnbnd  9025  expnlbnd  9026  expnlbnd2  9027  expaddd  9036  expmuld  9037  expclzapd  9039  expap0d  9040  expnegapd  9041  exprecapd  9042  expp1zapd  9043  expm1apd  9044  sqdivapd  9047  mulexpd  9049  expge0d  9052  expge1d  9053  reexpclzapd  9058  leexp2ad  9062  mulreap  9092  cjreb  9094  cjap  9134  cnrecnv  9138  cjdivapd  9195  redivapd  9201  imdivapd  9202
  Copyright terms: Public domain W3C validator