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

Theorem syl3anc 1135
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl111anc.4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3anc  |-  ( ph  ->  ta )

Proof of Theorem syl3anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1084 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 syl111anc.4 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
64, 5syl 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 885
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 887
This theorem is referenced by:  syl112anc  1139  syl121anc  1140  syl211anc  1141  syl113anc  1147  syl131anc  1148  syl311anc  1149  syld3an3  1180  3jaod  1199  mpd3an23  1234  stoic4a  1321  rspc3ev  2666  sbciedf  2798  euotd  3991  ordelord  4118  wetriext  4301  releldm  4569  relelrn  4570  f1imass  5413  ovmpt2dxf  5626  ovmpt2df  5632  fovrnd  5645  offval  5719  fnofval  5721  caoftrn  5736  offval3  5761  tfrlemisucaccv  5939  tfrlemiubacc  5944  rdgss  5970  rdgisuc1  5971  rdgisucinc  5972  freccl  5993  en2d  6248  en3d  6249  dom3d  6254  ssdomg  6258  f1imaen2g  6273  2dom  6285  cnven  6288  phpelm  6328  fidifsnen  6331  fidifsnid  6332  dif1en  6337  diffisn  6350  addcmpblnq  6465  addassnqg  6480  distrnqg  6485  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltaddnq  6505  ltexnqq  6506  prarloclemarch  6516  ltrnqg  6518  addcmpblnq0  6541  nnanq0  6556  distrnq0  6557  addassnq0  6560  prarloclemlt  6591  prarloclemcalc  6600  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  addlocprlemgt  6632  appdivnq  6661  prmuloclemcalc  6663  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  ltaprlem  6716  ltaprg  6717  addextpr  6719  recexprlem1ssu  6732  aptipr  6739  ltmprr  6740  caucvgprlemcanl  6742  cauappcvgprlemopl  6744  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprprlemloccalc  6782  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemloc  6801  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  ltsrprg  6832  distrsrg  6844  lttrsr  6847  ltsosr  6849  1idsr  6853  ltasrg  6855  recexgt0sr  6858  mulgt0sr  6862  mulextsr1lem  6864  srpospr  6867  prsradd  6870  prsrlt  6871  caucvgsrlemoffval  6880  caucvgsrlemoffgt1  6883  caucvgsrlemoffres  6884  caucvgsr  6886  pitoregt0  6925  recidpirqlemcalc  6933  axmulass  6947  axdistr  6948  rereceu  6963  recriota  6964  addassd  7049  mulassd  7050  adddid  7051  adddird  7052  lelttr  7106  letrd  7138  lelttrd  7139  lttrd  7140  mul12d  7165  mul32d  7166  mul31d  7167  add12d  7178  add32d  7179  cnegexlem3  7188  addcand  7195  addcan2d  7196  pncan  7217  pncan3  7219  subcan2  7236  subsub2  7239  subsub4  7244  npncan3  7249  pnpcan  7250  pnncan  7252  addsub4  7254  subaddd  7340  subadd2d  7341  addsubassd  7342  addsubd  7343  subadd23d  7344  addsub12d  7345  npncand  7346  nppcand  7347  nppcan2d  7348  nppcan3d  7349  subsubd  7350  subsub2d  7351  subsub3d  7352  subsub4d  7353  sub32d  7354  nnncand  7355  nnncan1d  7356  nnncan2d  7357  npncan3d  7358  pnpcand  7359  pnpcan2d  7360  pnncand  7361  ppncand  7362  subcand  7363  subcan2d  7364  subcanad  7365  subcan2ad  7367  subdid  7411  subdird  7412  ltadd2  7416  ltadd2d  7418  ltletrd  7420  ltsubadd  7427  lesubadd  7429  ltaddsub  7431  leaddsub  7433  le2add  7439  lt2add  7440  ltleadd  7441  lesub1  7451  lesub2  7452  ltsub1  7453  ltsub2  7454  lt2sub  7455  le2sub  7456  subge0  7470  lesub0  7474  ltadd1d  7529  leadd1d  7530  leadd2d  7531  ltsubaddd  7532  lesubaddd  7533  ltsubadd2d  7534  lesubadd2d  7535  ltaddsubd  7536  ltaddsub2d  7537  leaddsub2d  7538  subled  7539  lesubd  7540  ltsub23d  7541  ltsub13d  7542  lesub1d  7543  lesub2d  7544  ltsub1d  7545  ltsub2d  7546  gt0add  7564  apcotr  7598  apadd1  7599  addext  7601  mulext1  7603  mulext  7605  gtapd  7626  leltapd  7628  subap0d  7631  mulap0  7635  divvalap  7653  divcanap2  7659  diveqap0  7661  divrecap  7667  divassap  7669  divdirap  7674  divcanap3  7675  div11ap  7677  rec11ap  7686  divmuldivap  7688  divdivdivap  7689  divmuleqap  7693  dmdcanap  7698  ddcanap  7702  divadddivap  7703  divsubdivap  7704  redivclap  7707  apmul1  7764  divclapd  7765  divcanap1d  7766  divcanap2d  7767  divrecapd  7768  divrecap2d  7769  divcanap3d  7770  divcanap4d  7771  diveqap0d  7772  diveqap1d  7773  diveqap1ad  7774  diveqap0ad  7775  divap0bd  7777  divnegapd  7778  divneg2apd  7779  div2negapd  7780  redivclapd  7808  ltmul12a  7826  lemul12b  7827  lt2mul2div  7845  ltdiv2  7853  ltdiv23  7858  avglt1  8163  avglt2  8164  lt2halvesd  8172  div4p1lem1div2  8177  zltp1le  8298  elz2  8312  zdivmul  8330  uztrn  8489  eluzsub  8502  uz3m2nn  8515  qaddcl  8570  cnref1o  8582  ltdiv2d  8646  lediv2d  8647  divlt1lt  8650  divle1le  8651  ledivge1le  8652  ltmulgt11d  8658  ltmulgt12d  8659  gt0divd  8660  ge0divd  8661  rpgecld  8662  ltmul1d  8664  ltmul2d  8665  lemul1d  8666  lemul2d  8667  ltdiv1d  8668  lediv1d  8669  ltmuldivd  8670  ltmuldiv2d  8671  lemuldivd  8672  lemuldiv2d  8673  ltdivmuld  8674  ltdivmul2d  8675  ledivmuld  8676  ledivmul2d  8677  ltdiv23d  8683  lediv23d  8684  xrltso  8717  xrlelttr  8722  xrlttrd  8725  xrlelttrd  8726  xrltletrd  8727  xrletrd  8728  xrre3  8735  ixxss1  8773  ixxss2  8774  ixxss12  8775  iooshf  8821  icoshftf1o  8859  ioodisj  8861  fznlem  8905  fzdifsuc  8943  fzrev  8946  fzrevral2  8968  elfz0fzfz0  8983  elfzmlbp  8990  fzctr  8991  elfzole1  9011  elfzolt2  9012  fzoss2  9028  fzospliti  9032  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  fzoaddel  9048  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  ssfzo12bi  9081  elfzonelfzo  9086  fvinim0ffz  9096  qbtwnzlemex  9105  rebtwn2zlemstep  9107  rebtwn2z  9109  flqge  9124  2tnp1ge0ge0  9143  intfracq  9162  flqdiv  9163  modqval  9166  modqcld  9170  modqmulnn  9184  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgsuc  9201  frecfzen2  9204  iseqval  9220  iseqp1  9225  monoord  9235  expinnval  9258  expnegap0  9263  rpexpcl  9274  expnegzap  9289  expgt1  9293  mulexpzap  9295  exprecap  9296  expaddzaplem  9298  expaddzap  9299  expmul  9300  expmulzap  9301  expdivap  9305  ltexp2a  9306  leexp2a  9307  leexp2r  9308  leexp1a  9309  bernneq2  9370  bernneq3  9371  expnbnd  9372  expnlbnd  9373  expnlbnd2  9374  expaddd  9383  expmuld  9384  expclzapd  9386  expap0d  9387  expnegapd  9388  exprecapd  9389  expp1zapd  9390  expm1apd  9391  sqdivapd  9394  mulexpd  9396  expge0d  9399  expge1d  9400  reexpclzapd  9405  leexp2ad  9409  shftfvalg  9419  mulreap  9464  cjreb  9466  cjap  9506  cnrecnv  9510  cjdivapd  9568  redivapd  9574  imdivapd  9575  resqrexlemdecn  9610  absexpzap  9676  abslt  9684  absle  9685  elicc4abs  9690  abs3lem  9707  fzomaxdiflem  9708  cau3lem  9710  amgm2  9714  abssubge0d  9772  abssuble0d  9773  absdifltd  9774  absdifled  9775  absdivapd  9791  abs3difd  9796  qdenre  9798  climshftlemg  9823  climshft2  9827  addcn2  9831  mulcn2  9833  cn1lem  9834  climadd  9846  climmul  9847  climsub  9848  climsqz  9855  climsqz2  9856  climrecvg1n  9867  climcvg1nlem  9868  nn0seqcvgd  9880
  Copyright terms: Public domain W3C validator