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  3981  ordelord  4083  releldm  4511  relelrn  4512  f1imass  5354  ovmpt2dxf  5565  ovmpt2df  5571  fovrnd  5584  offval  5658  fnofval  5660  caoftrn  5675  offval3  5700  tfrlemisucaccv  5877  tfrlemiubacc  5882  rdgss  5907  rdgisuc1  5908  rdgisucinc  5909  en2d  6177  en3d  6178  dom3d  6183  ssdomg  6187  f1imaen2g  6202  2dom  6214  cnven  6217  addcmpblnq  6344  addassnqg  6359  distrnqg  6364  ltsonq  6375  ltanqg  6377  ltmnqg  6378  ltaddnq  6383  ltexnqq  6384  prarloclemarch  6394  ltrnqg  6396  addcmpblnq0  6418  nnanq0  6433  distrnq0  6434  addassnq0  6437  prarloclemlt  6468  prarloclemcalc  6477  addnqprllem  6503  addnqprulem  6504  addnqprl  6505  addnqpru  6506  addlocprlemgt  6510  appdivnq  6534  prmuloclemcalc  6536  mulnqprl  6539  mulnqpru  6540  mullocprlem  6541  distrlem4prl  6550  distrlem4pru  6551  ltprordil  6555  ltexprlemopl  6565  ltexprlemopu  6567  ltexprlemloc  6571  ltexprlemru  6576  addcanprleml  6578  addcanprlemu  6579  ltaprlem  6581  ltaprg  6582  addextpr  6583  recexprlem1ssu  6596  aptipr  6603  ltmprr  6604  addcmpblnr  6619  mulcmpblnrlemg  6620  mulcmpblnr  6621  ltsrprg  6627  distrsrg  6639  lttrsr  6642  ltsosr  6644  1idsr  6648  ltasrg  6650  recexgt0sr  6653  mulgt0sr  6656  mulextsr1lem  6658  axmulass  6709  axdistr  6710  addassd  6799  mulassd  6800  adddid  6801  adddird  6802  lelttr  6855  letrd  6887  lelttrd  6888  lttrd  6889  mul12d  6914  mul32d  6915  mul31d  6916  add12d  6927  add32d  6928  cnegexlem3  6937  addcand  6944  addcan2d  6945  pncan  6966  pncan3  6968  subcan2  6984  subsub2  6987  subsub4  6992  npncan3  6997  pnpcan  6998  pnncan  7000  addsub4  7002  subaddd  7088  subadd2d  7089  addsubassd  7090  addsubd  7091  subadd23d  7092  addsub12d  7093  npncand  7094  nppcand  7095  nppcan2d  7096  nppcan3d  7097  subsubd  7098  subsub2d  7099  subsub3d  7100  subsub4d  7101  sub32d  7102  nnncand  7103  nnncan1d  7104  nnncan2d  7105  npncan3d  7106  pnpcand  7107  pnpcan2d  7108  pnncand  7109  ppncand  7110  subcand  7111  subcan2d  7112  subcanad  7113  subcan2ad  7115  subdid  7159  subdird  7160  ltadd2  7164  ltadd2d  7166  ltletrd  7168  ltsubadd  7174  lesubadd  7176  ltaddsub  7178  leaddsub  7180  le2add  7186  lt2add  7187  ltleadd  7188  lesub1  7198  lesub2  7199  ltsub1  7200  ltsub2  7201  lt2sub  7202  le2sub  7203  subge0  7217  lesub0  7221  ltadd1d  7276  leadd1d  7277  leadd2d  7278  ltsubaddd  7279  lesubaddd  7280  ltsubadd2d  7281  lesubadd2d  7282  ltaddsubd  7283  ltaddsub2d  7284  leaddsub2d  7285  subled  7286  lesubd  7287  ltsub23d  7288  ltsub13d  7289  lesub1d  7290  lesub2d  7291  ltsub1d  7292  ltsub2d  7293  gt0add  7309  apcotr  7343  apadd1  7344  addext  7346  mulext1  7348  mulext  7350  mulap0  7369  divvalap  7387  divcanap2  7393  diveqap0  7395  divrecap  7401  divassap  7403  divdirap  7408  divcanap3  7409  div11ap  7411  rec11ap  7420  divmuldivap  7422  divdivdivap  7423  divmuleqap  7427  dmdcanap  7432  ddcanap  7436  divadddivap  7437  divsubdivap  7438  redivclap  7441  apmul1  7498  divclapd  7499  divcanap1d  7500  divcanap2d  7501  divrecapd  7502  divrecap2d  7503  divcanap3d  7504  divcanap4d  7505  diveqap0d  7506  diveqap1d  7507  diveqap1ad  7508  diveqap0ad  7509  divap0bd  7511  divnegapd  7512  divneg2apd  7513  div2negapd  7514  redivclapd  7541  ltmul12a  7558  lemul12b  7559  lt2mul2div  7577  ltdiv2  7585  ltdiv23  7590  avglt1  7890  avglt2  7891  lt2halvesd  7899  zltp1le  8024  elz2  8038  zdivmul  8055  uztrn  8214  eluzsub  8227  uz3m2nn  8240  qaddcl  8295  ltdiv2d  8368  lediv2d  8369  ltmulgt11d  8376  ltmulgt12d  8377  gt0divd  8378  ge0divd  8379  rpgecld  8380  ltmul1d  8382  ltmul2d  8383  lemul1d  8384  lemul2d  8385  ltdiv1d  8386  lediv1d  8387  ltmuldivd  8388  ltmuldiv2d  8389  lemuldivd  8390  lemuldiv2d  8391  ltdivmuld  8392  ltdivmul2d  8393  ledivmuld  8394  ledivmul2d  8395  ltdiv23d  8401  lediv23d  8402  xrltso  8435  xrlelttr  8440  xrlttrd  8443  xrlelttrd  8444  xrltletrd  8445  xrletrd  8446  xrre3  8453  ixxss1  8491  ixxss2  8492  ixxss12  8493  iooshf  8539  icoshftf1o  8577  ioodisj  8579  fznlem  8621  fzdifsuc  8659  fzrev  8662  fzrevral2  8684  elfz0fzfz0  8699  elfzmlbp  8706  fzctr  8707  elfzole1  8727  elfzolt2  8728  fzoss2  8744  fzospliti  8748  fzo1fzo0n0  8755  elfzo0z  8756  fzofzim  8760  fzoaddel  8764  eluzgtdifelfzo  8769  elfzodifsumelfzo  8773  ssfzo12bi  8797  elfzonelfzo  8802  frecfzen2  8823
  Copyright terms: Public domain W3C validator