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

Theorem syl3anc 1146
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 1095 . 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 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  syl112anc  1150  syl121anc  1151  syl211anc  1152  syl113anc  1158  syl131anc  1159  syl311anc  1160  syld3an3  1191  3jaod  1210  mpd3an23  1245  stoic4a  1337  rspc3ev  2688  sbciedf  2820  euotd  4018  ordelord  4145  wetriext  4328  releldm  4596  relelrn  4597  f1imass  5440  ovmpt2dxf  5653  ovmpt2df  5659  fovrnd  5672  offval  5746  fnofval  5748  caoftrn  5763  offval3  5788  tfrlemisucaccv  5969  tfrlemiubacc  5974  rdgss  6000  rdgisuc1  6001  rdgisucinc  6002  freccl  6023  en2d  6278  en3d  6279  dom3d  6284  ssdomg  6288  f1imaen2g  6303  2dom  6315  cnven  6318  phpelm  6358  fidifsnen  6361  fidifsnid  6362  dif1en  6367  diffisn  6380  addcmpblnq  6522  addassnqg  6537  distrnqg  6542  ltsonq  6553  ltanqg  6555  ltmnqg  6556  ltaddnq  6562  ltexnqq  6563  prarloclemarch  6573  ltrnqg  6575  addcmpblnq0  6598  nnanq0  6613  distrnq0  6614  addassnq0  6617  prarloclemlt  6648  prarloclemcalc  6657  addnqprllem  6682  addnqprulem  6683  addnqprl  6684  addnqpru  6685  addlocprlemgt  6689  appdivnq  6718  prmuloclemcalc  6720  mulnqprl  6723  mulnqpru  6724  mullocprlem  6725  distrlem4prl  6739  distrlem4pru  6740  ltprordil  6744  ltexprlemopl  6756  ltexprlemopu  6758  ltexprlemloc  6762  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  ltaprlem  6773  ltaprg  6774  addextpr  6776  recexprlem1ssu  6789  aptipr  6796  ltmprr  6797  caucvgprlemcanl  6799  cauappcvgprlemopl  6801  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  cauappcvgprlem1  6814  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemloc  6830  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprprlemloccalc  6839  caucvgprprlemml  6849  caucvgprprlemopl  6852  caucvgprprlemloc  6858  caucvgprprlemexb  6862  caucvgprprlemaddq  6863  caucvgprprlem1  6864  caucvgprprlem2  6865  addcmpblnr  6881  mulcmpblnrlemg  6882  mulcmpblnr  6883  ltsrprg  6889  distrsrg  6901  lttrsr  6904  ltsosr  6906  1idsr  6910  ltasrg  6912  recexgt0sr  6915  mulgt0sr  6919  mulextsr1lem  6921  srpospr  6924  prsradd  6927  prsrlt  6928  caucvgsrlemoffval  6937  caucvgsrlemoffgt1  6940  caucvgsrlemoffres  6941  caucvgsr  6943  pitoregt0  6982  recidpirqlemcalc  6990  axmulass  7004  axdistr  7005  rereceu  7020  recriota  7021  addassd  7106  mulassd  7107  adddid  7108  adddird  7109  lelttr  7164  letrd  7198  lelttrd  7199  lttrd  7200  mul12d  7225  mul32d  7226  mul31d  7227  add12d  7240  add32d  7241  cnegexlem3  7250  addcand  7257  addcan2d  7258  pncan  7279  pncan3  7281  subcan2  7298  subsub2  7301  subsub4  7306  npncan3  7311  pnpcan  7312  pnncan  7314  addsub4  7316  subaddd  7402  subadd2d  7403  addsubassd  7404  addsubd  7405  subadd23d  7406  addsub12d  7407  npncand  7408  nppcand  7409  nppcan2d  7410  nppcan3d  7411  subsubd  7412  subsub2d  7413  subsub3d  7414  subsub4d  7415  sub32d  7416  nnncand  7417  nnncan1d  7418  nnncan2d  7419  npncan3d  7420  pnpcand  7421  pnpcan2d  7422  pnncand  7423  ppncand  7424  subcand  7425  subcan2d  7426  subcanad  7427  subcan2ad  7429  subdid  7482  subdird  7483  ltadd2  7487  ltadd2d  7489  ltletrd  7491  ltsubadd  7500  lesubadd  7502  ltaddsub  7504  leaddsub  7506  le2add  7512  lt2add  7513  ltleadd  7514  lesub1  7524  lesub2  7525  ltsub1  7526  ltsub2  7527  lt2sub  7528  le2sub  7529  subge0  7543  lesub0  7547  ltadd1d  7602  leadd1d  7603  leadd2d  7604  ltsubaddd  7605  lesubaddd  7606  ltsubadd2d  7607  lesubadd2d  7608  ltaddsubd  7609  ltaddsub2d  7610  leaddsub2d  7611  subled  7612  lesubd  7613  ltsub23d  7614  ltsub13d  7615  lesub1d  7616  lesub2d  7617  ltsub1d  7618  ltsub2d  7619  gt0add  7637  apcotr  7671  apadd1  7672  addext  7674  mulext1  7676  mulext  7678  gtapd  7699  leltapd  7701  subap0d  7704  mulap0  7708  divvalap  7726  divcanap2  7732  diveqap0  7734  divrecap  7740  divassap  7742  divdirap  7747  divcanap3  7748  div11ap  7750  rec11ap  7760  divmuldivap  7762  divdivdivap  7763  divmuleqap  7767  dmdcanap  7772  ddcanap  7776  divadddivap  7777  divsubdivap  7778  redivclap  7781  apmul1  7838  divclapd  7839  divcanap1d  7840  divcanap2d  7841  divrecapd  7842  divrecap2d  7843  divcanap3d  7844  divcanap4d  7845  diveqap0d  7846  diveqap1d  7847  diveqap1ad  7848  diveqap0ad  7849  divap0bd  7851  divnegapd  7852  divneg2apd  7853  div2negapd  7854  redivclapd  7882  ltmul12a  7900  lemul12b  7901  lt2mul2div  7919  ltdiv2  7927  ltdiv23  7932  avglt1  8219  avglt2  8220  lt2halvesd  8228  div4p1lem1div2  8234  zltp1le  8355  elz2  8369  zdivmul  8387  uztrn  8584  eluzsub  8597  uz3m2nn  8610  qaddcl  8666  cnref1o  8679  ltdiv2d  8743  lediv2d  8744  divlt1lt  8747  divle1le  8748  ledivge1le  8749  ltmulgt11d  8755  ltmulgt12d  8756  gt0divd  8757  ge0divd  8758  rpgecld  8759  ltmul1d  8761  ltmul2d  8762  lemul1d  8763  lemul2d  8764  ltdiv1d  8765  lediv1d  8766  ltmuldivd  8767  ltmuldiv2d  8768  lemuldivd  8769  lemuldiv2d  8770  ltdivmuld  8771  ltdivmul2d  8772  ledivmuld  8773  ledivmul2d  8774  ltdiv23d  8780  lediv23d  8781  addlelt  8785  xrltso  8817  xrlelttr  8822  xrlttrd  8825  xrlelttrd  8826  xrltletrd  8827  xrletrd  8828  xrre3  8835  ixxss1  8873  ixxss2  8874  ixxss12  8875  iooshf  8921  icoshftf1o  8959  ioodisj  8961  zltaddlt1le  8974  fznlem  9006  fzdifsuc  9044  fzrev  9047  fzrevral2  9069  elfz0fzfz0  9084  elfzmlbp  9091  fzctr  9092  elfzole1  9112  elfzolt2  9113  fzoss2  9129  fzospliti  9133  fzo1fzo0n0  9140  elfzo0z  9141  fzofzim  9145  fzoaddel  9149  eluzgtdifelfzo  9154  elfzodifsumelfzo  9158  ssfzo12bi  9182  elfzonelfzo  9187  fvinim0ffz  9197  qbtwnzlemex  9206  rebtwn2zlemstep  9208  rebtwn2z  9210  qbtwnxr  9213  flqge  9231  2tnp1ge0ge0  9250  intfracq  9269  flqdiv  9270  modqval  9273  modqcld  9277  modqmulnn  9291  zmodcl  9293  zmodfz  9295  modqid  9298  zmodid2  9301  modqabs  9306  modqcyc  9308  modqadd1  9310  modqaddabs  9311  modqaddmod  9312  mulp1mod1  9314  modqmuladd  9315  modqmuladdim  9316  modqmuladdnn0  9317  m1modnnsub1  9319  modqltm1p1mod  9325  modqmul1  9326  modqsubmod  9331  modqsubmodmod  9332  q2txmodxeq0  9333  modaddmodup  9336  modqmulmod  9338  modqaddmulmod  9340  modqdi  9341  modqsubdir  9342  addmodlteq  9347  frecuzrdgrrn  9357  frec2uzrdg  9358  frecuzrdgsuc  9364  frecfzen2  9367  iseqval  9383  iseqp1  9388  monoord  9398  expinnval  9422  expnegap0  9427  rpexpcl  9438  expnegzap  9453  expgt1  9457  mulexpzap  9459  exprecap  9460  expaddzaplem  9462  expaddzap  9463  expmul  9464  expmulzap  9465  expdivap  9470  ltexp2a  9471  leexp2a  9472  leexp2r  9473  leexp1a  9474  bernneq2  9537  bernneq3  9538  expnbnd  9539  expnlbnd  9540  expnlbnd2  9541  expaddd  9550  expmuld  9551  expclzapd  9553  expap0d  9554  expnegapd  9555  exprecapd  9556  expp1zapd  9557  expm1apd  9558  sqdivapd  9561  mulexpd  9563  expge0d  9566  expge1d  9567  sqoddm1div8  9568  reexpclzapd  9573  leexp2ad  9577  facwordi  9607  faclbnd3  9610  facavg  9613  bcval  9616  bccmpl  9621  bc0k  9623  ibcval5  9630  bcpasc  9633  shftfvalg  9646  mulreap  9691  cjreb  9693  cjap  9733  cnrecnv  9737  cjdivapd  9795  redivapd  9801  imdivapd  9802  resqrexlemdecn  9838  absexpzap  9906  abslt  9914  absle  9915  elicc4abs  9920  abs3lem  9937  fzomaxdiflem  9938  cau3lem  9940  amgm2  9944  abssubge0d  10002  abssuble0d  10003  absdifltd  10004  absdifled  10005  absdivapd  10021  abs3difd  10026  qdenre  10028  climshftlemg  10053  climshft2  10057  addcn2  10061  mulcn2  10063  cn1lem  10064  climadd  10076  climmul  10077  climsub  10078  climsqz  10085  climsqz2  10086  climrecvg1n  10097  climcvg1nlem  10098  dvdsval3  10111  nndivdvds  10113  summodnegmod  10137  modmulconst  10138  dvds2subd  10142  dvdsmultr1d  10145  dvdsmultr2  10146  dvdsabseq  10158  dvdsfac  10171  dvdsmod  10173  oddge22np1  10192  ltoddhalfle  10204  halfleoddlt  10205  nn0ehalf  10214  nno  10217  nn0oddm1d2  10220  pw2dvdseulemle  10234  nn0seqcvgd  10242
  Copyright terms: Public domain W3C validator