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  6425  nnanq0  6440  distrnq0  6441  addassnq0  6444  prarloclemlt  6475  prarloclemcalc  6484  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  addlocprlemgt  6516  appdivnq  6543  prmuloclemcalc  6545  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  ltaprlem  6590  ltaprg  6591  addextpr  6592  recexprlem1ssu  6605  aptipr  6612  ltmprr  6613  cauappcvgprlemcan  6615  cauappcvgprlemopl  6617  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  ltsrprg  6655  distrsrg  6667  lttrsr  6670  ltsosr  6672  1idsr  6676  ltasrg  6678  recexgt0sr  6681  mulgt0sr  6684  mulextsr1lem  6686  axmulass  6737  axdistr  6738  addassd  6827  mulassd  6828  adddid  6829  adddird  6830  lelttr  6883  letrd  6915  lelttrd  6916  lttrd  6917  mul12d  6942  mul32d  6943  mul31d  6944  add12d  6955  add32d  6956  cnegexlem3  6965  addcand  6972  addcan2d  6973  pncan  6994  pncan3  6996  subcan2  7012  subsub2  7015  subsub4  7020  npncan3  7025  pnpcan  7026  pnncan  7028  addsub4  7030  subaddd  7116  subadd2d  7117  addsubassd  7118  addsubd  7119  subadd23d  7120  addsub12d  7121  npncand  7122  nppcand  7123  nppcan2d  7124  nppcan3d  7125  subsubd  7126  subsub2d  7127  subsub3d  7128  subsub4d  7129  sub32d  7130  nnncand  7131  nnncan1d  7132  nnncan2d  7133  npncan3d  7134  pnpcand  7135  pnpcan2d  7136  pnncand  7137  ppncand  7138  subcand  7139  subcan2d  7140  subcanad  7141  subcan2ad  7143  subdid  7187  subdird  7188  ltadd2  7192  ltadd2d  7194  ltletrd  7196  ltsubadd  7202  lesubadd  7204  ltaddsub  7206  leaddsub  7208  le2add  7214  lt2add  7215  ltleadd  7216  lesub1  7226  lesub2  7227  ltsub1  7228  ltsub2  7229  lt2sub  7230  le2sub  7231  subge0  7245  lesub0  7249  ltadd1d  7304  leadd1d  7305  leadd2d  7306  ltsubaddd  7307  lesubaddd  7308  ltsubadd2d  7309  lesubadd2d  7310  ltaddsubd  7311  ltaddsub2d  7312  leaddsub2d  7313  subled  7314  lesubd  7315  ltsub23d  7316  ltsub13d  7317  lesub1d  7318  lesub2d  7319  ltsub1d  7320  ltsub2d  7321  gt0add  7337  apcotr  7371  apadd1  7372  addext  7374  mulext1  7376  mulext  7378  mulap0  7397  divvalap  7415  divcanap2  7421  diveqap0  7423  divrecap  7429  divassap  7431  divdirap  7436  divcanap3  7437  div11ap  7439  rec11ap  7448  divmuldivap  7450  divdivdivap  7451  divmuleqap  7455  dmdcanap  7460  ddcanap  7464  divadddivap  7465  divsubdivap  7466  redivclap  7469  apmul1  7526  divclapd  7527  divcanap1d  7528  divcanap2d  7529  divrecapd  7530  divrecap2d  7531  divcanap3d  7532  divcanap4d  7533  diveqap0d  7534  diveqap1d  7535  diveqap1ad  7536  diveqap0ad  7537  divap0bd  7539  divnegapd  7540  divneg2apd  7541  div2negapd  7542  redivclapd  7569  ltmul12a  7587  lemul12b  7588  lt2mul2div  7606  ltdiv2  7614  ltdiv23  7619  avglt1  7920  avglt2  7921  lt2halvesd  7929  zltp1le  8054  elz2  8068  zdivmul  8086  uztrn  8245  eluzsub  8258  uz3m2nn  8271  qaddcl  8326  cnref1o  8337  ltdiv2d  8400  lediv2d  8401  ltmulgt11d  8408  ltmulgt12d  8409  gt0divd  8410  ge0divd  8411  rpgecld  8412  ltmul1d  8414  ltmul2d  8415  lemul1d  8416  lemul2d  8417  ltdiv1d  8418  lediv1d  8419  ltmuldivd  8420  ltmuldiv2d  8421  lemuldivd  8422  lemuldiv2d  8423  ltdivmuld  8424  ltdivmul2d  8425  ledivmuld  8426  ledivmul2d  8427  ltdiv23d  8433  lediv23d  8434  xrltso  8467  xrlelttr  8472  xrlttrd  8475  xrlelttrd  8476  xrltletrd  8477  xrletrd  8478  xrre3  8485  ixxss1  8523  ixxss2  8524  ixxss12  8525  iooshf  8571  icoshftf1o  8609  ioodisj  8611  fznlem  8655  fzdifsuc  8693  fzrev  8696  fzrevral2  8718  elfz0fzfz0  8733  elfzmlbp  8740  fzctr  8741  elfzole1  8761  elfzolt2  8762  fzoss2  8778  fzospliti  8782  fzo1fzo0n0  8789  elfzo0z  8790  fzofzim  8794  fzoaddel  8798  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  ssfzo12bi  8831  elfzonelfzo  8836  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgsuc  8862  frecfzen2  8865  iseqval  8880  iseqp1  8884  expinnval  8892  expnegap0  8897  rpexpcl  8908  expnegzap  8923  expgt1  8927  mulexpzap  8929  exprecap  8930  expaddzaplem  8932  expaddzap  8933  expmul  8934  expmulzap  8935  expdivap  8939  ltexp2a  8940  leexp2a  8941  leexp2r  8942  leexp1a  8943  bernneq2  9003  bernneq3  9004  expnbnd  9005  expnlbnd  9006  expnlbnd2  9007  expaddd  9016  expmuld  9017  expclzapd  9019  expap0d  9020  expnegapd  9021  exprecapd  9022  expp1zapd  9023  expm1apd  9024  sqdivapd  9027  mulexpd  9029  expge0d  9032  expge1d  9033  reexpclzapd  9038  leexp2ad  9042  mulreap  9072  cjreb  9074  cjap  9114  cnrecnv  9118  cjdivapd  9175  redivapd  9181  imdivapd  9182
  Copyright terms: Public domain W3C validator