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

Theorem syl3anc 1217
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 1162 . 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 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  syl112anc  1221  syl121anc  1222  syl211anc  1223  syl113anc  1229  syl131anc  1230  syl311anc  1231  syld3an3  1262  3jaod  1283  mpd3an23  1318  stoic4a  1409  rspc3ev  2807  sbciedf  2945  euotd  4180  ordelord  4307  wetriext  4495  releldm  4778  relelrn  4779  f1imass  5679  ovmpodxf  5900  ovmpodf  5906  fovrnd  5919  offval  5993  caoftrn  6011  offval3  6036  fnmpoovd  6116  tfrlemisucaccv  6226  tfrlemiubacc  6231  tfr1onlemsucaccv  6242  tfr1onlembfn  6245  tfrcllemsucaccv  6255  tfrcllembfn  6258  rdgss  6284  rdgisuc1  6285  rdgisucinc  6286  frecrdg  6309  mapsspm  6580  en2d  6666  en3d  6667  dom3d  6672  ssdomg  6676  f1imaen2g  6691  2dom  6703  cnven  6706  mapen  6744  mapxpen  6746  phpelm  6764  fidifsnen  6768  dif1en  6777  dif1enen  6778  diffisn  6791  isinfinf  6795  unfidisj  6814  unfiin  6818  tpfidisj  6820  xpfi  6822  fisseneq  6824  phpeqd  6825  ssfirab  6826  fnfi  6829  f1dmvrnfibi  6836  iunfidisj  6838  f1finf1o  6839  en1eqsn  6840  fidcenumlemr  6847  updjudhcoinlf  6969  updjudhcoinrg  6970  difinfinf  6990  en2eleq  7064  en2other2  7065  dju1en  7082  djuassen  7086  xpdjuen  7087  addcmpblnq  7195  addassnqg  7210  distrnqg  7215  ltsonq  7226  ltanqg  7228  ltmnqg  7229  ltaddnq  7235  ltexnqq  7236  prarloclemarch  7246  ltrnqg  7248  addcmpblnq0  7271  nnanq0  7286  distrnq0  7287  addassnq0  7290  prarloclemlt  7321  prarloclemcalc  7330  addnqprllem  7355  addnqprulem  7356  addnqprl  7357  addnqpru  7358  addlocprlemgt  7362  appdivnq  7391  prmuloclemcalc  7393  mulnqprl  7396  mulnqpru  7397  mullocprlem  7398  distrlem4prl  7412  distrlem4pru  7413  ltprordil  7417  ltexprlemopl  7429  ltexprlemopu  7431  ltexprlemloc  7435  ltexprlemru  7440  addcanprleml  7442  addcanprlemu  7443  ltaprlem  7446  ltaprg  7447  addextpr  7449  recexprlem1ssu  7462  aptipr  7469  ltmprr  7470  caucvgprlemcanl  7472  cauappcvgprlemopl  7474  cauappcvgprlemdisj  7479  cauappcvgprlemloc  7480  cauappcvgprlemladdfu  7482  cauappcvgprlemladdru  7484  cauappcvgprlemladdrl  7485  cauappcvgprlem1  7487  caucvgprlemm  7496  caucvgprlemopl  7497  caucvgprlemloc  7503  caucvgprlemladdfu  7505  caucvgprlemladdrl  7506  caucvgprprlemloccalc  7512  caucvgprprlemml  7522  caucvgprprlemopl  7525  caucvgprprlemloc  7531  caucvgprprlemexb  7535  caucvgprprlemaddq  7536  caucvgprprlem1  7537  caucvgprprlem2  7538  suplocexprlemmu  7546  suplocexprlemru  7547  addcmpblnr  7567  mulcmpblnrlemg  7568  mulcmpblnr  7569  ltsrprg  7575  distrsrg  7587  lttrsr  7590  ltsosr  7592  1idsr  7596  ltasrg  7598  recexgt0sr  7601  mulgt0sr  7606  mulextsr1lem  7608  srpospr  7611  prsradd  7614  prsrlt  7615  caucvgsrlemoffval  7624  caucvgsrlemoffgt1  7627  caucvgsrlemoffres  7628  caucvgsr  7630  ltpsrprg  7631  map2psrprg  7633  suplocsrlemb  7634  suplocsrlempr  7635  suplocsrlem  7636  pitoregt0  7677  recidpirqlemcalc  7685  axmulass  7701  axdistr  7702  rereceu  7717  recriota  7718  addassd  7808  mulassd  7809  adddid  7810  adddird  7811  lelttr  7872  letrd  7906  lelttrd  7907  lttrd  7908  mul12d  7934  mul32d  7935  mul31d  7936  add12d  7949  add32d  7950  cnegexlem3  7959  addcand  7966  addcan2d  7967  pncan  7988  pncan3  7990  subcan2  8007  subsub2  8010  subsub4  8015  npncan3  8020  pnpcan  8021  pnncan  8023  addsub4  8025  subaddd  8111  subadd2d  8112  addsubassd  8113  addsubd  8114  subadd23d  8115  addsub12d  8116  npncand  8117  nppcand  8118  nppcan2d  8119  nppcan3d  8120  subsubd  8121  subsub2d  8122  subsub3d  8123  subsub4d  8124  sub32d  8125  nnncand  8126  nnncan1d  8127  nnncan2d  8128  npncan3d  8129  pnpcand  8130  pnpcan2d  8131  pnncand  8132  ppncand  8133  subcand  8134  subcan2d  8135  subcanad  8136  subcan2ad  8138  subdid  8196  subdird  8197  ltadd2  8201  ltadd2d  8203  ltletrd  8205  ltsubadd  8214  lesubadd  8216  ltaddsub  8218  leaddsub  8220  le2add  8226  lt2add  8227  ltleadd  8228  lesub1  8238  lesub2  8239  ltsub1  8240  ltsub2  8241  lt2sub  8242  le2sub  8243  subge0  8257  lesub0  8261  ltadd1d  8320  leadd1d  8321  leadd2d  8322  ltsubaddd  8323  lesubaddd  8324  ltsubadd2d  8325  lesubadd2d  8326  ltaddsubd  8327  ltaddsub2d  8328  leaddsub2d  8329  subled  8330  lesubd  8331  ltsub23d  8332  ltsub13d  8333  lesub1d  8334  lesub2d  8335  ltsub1d  8336  ltsub2d  8337  gt0add  8355  apcotr  8389  apadd1  8390  addext  8392  mulext1  8394  mulext  8396  gtapd  8419  leltapd  8421  subap0d  8426  mulap0  8435  mul0eqap  8451  divvalap  8454  divcanap2  8460  diveqap0  8462  divrecap  8468  divassap  8470  divmulassap  8475  divmulasscomap  8476  divdirap  8477  divcanap3  8478  div11ap  8480  rec11ap  8490  divmuldivap  8492  divdivdivap  8493  divmuleqap  8497  dmdcanap  8502  ddcanap  8506  divadddivap  8507  divsubdivap  8508  redivclap  8511  apmul1  8568  divclapd  8570  divcanap1d  8571  divcanap2d  8572  divrecapd  8573  divrecap2d  8574  divcanap3d  8575  divcanap4d  8576  diveqap0d  8577  diveqap1d  8578  diveqap1ad  8579  diveqap0ad  8580  divap0bd  8582  divnegapd  8583  divneg2apd  8584  div2negapd  8585  redivclapd  8614  div2subap  8616  ltmul12a  8638  lemul12b  8639  lt2mul2div  8657  ltdiv2  8665  ltdiv23  8670  avglt1  8978  avglt2  8979  lt2halvesd  8987  div4p1lem1div2  8993  zltp1le  9128  elz2  9142  zdivmul  9161  uztrn  9362  eluzsub  9375  uz3m2nn  9391  qaddcl  9450  elpq  9463  cnref1o  9465  ltdiv2d  9533  lediv2d  9534  divlt1lt  9537  divle1le  9538  ledivge1le  9539  ltmulgt11d  9545  ltmulgt12d  9546  gt0divd  9547  ge0divd  9548  rpgecld  9549  ltmul1d  9551  ltmul2d  9552  lemul1d  9553  lemul2d  9554  ltdiv1d  9555  lediv1d  9556  ltmuldivd  9557  ltmuldiv2d  9558  lemuldivd  9559  lemuldiv2d  9560  ltdivmuld  9561  ltdivmul2d  9562  ledivmuld  9563  ledivmul2d  9564  ltdiv23d  9570  lediv23d  9571  addlelt  9581  xrltso  9608  xrlelttr  9615  xrlttrd  9618  xrlelttrd  9619  xrltletrd  9620  xrletrd  9621  xrre3  9631  xleadd1  9684  xltadd1  9685  xle2add  9688  xlt2add  9689  xlesubadd  9692  xadd4d  9694  ixxss1  9713  ixxss2  9714  ixxss12  9715  iooshf  9761  icoshftf1o  9800  ioodisj  9802  zltaddlt1le  9816  fznlem  9848  fzdifsuc  9888  fzrev  9891  fzrevral2  9913  elfz0fzfz0  9930  elfzmlbp  9936  fzctr  9937  elfzole1  9959  elfzolt2  9960  fzoss2  9976  fzospliti  9980  fzo1fzo0n0  9987  elfzo0z  9988  fzofzim  9992  fzoaddel  9996  eluzgtdifelfzo  10001  elfzodifsumelfzo  10005  ssfzo12bi  10029  elfzonelfzo  10034  fvinim0ffz  10045  rebtwn2zlemstep  10057  rebtwn2z  10059  qbtwnxr  10062  flqge  10082  2tnp1ge0ge0  10101  intfracq  10120  flqdiv  10121  modqval  10124  modqcld  10128  modqmulnn  10142  zmodcl  10144  zmodfz  10146  modqid  10149  zmodid2  10152  modqabs  10157  modqcyc  10159  modqadd1  10161  modqaddabs  10162  modqaddmod  10163  mulp1mod1  10165  modqmuladd  10166  modqmuladdim  10167  modqmuladdnn0  10168  m1modnnsub1  10170  modqltm1p1mod  10176  modqmul1  10177  modqsubmod  10182  modqsubmodmod  10183  q2txmodxeq0  10184  modaddmodup  10187  modqmulmod  10189  modqaddmulmod  10191  modqdi  10192  modqsubdir  10193  addmodlteq  10198  frecuzrdgrrn  10208  frec2uzrdg  10209  frecuzrdgrcl  10210  frecuzrdgsuc  10214  frecuzrdgrclt  10215  frecuzrdgg  10216  frecuzrdgsuctlem  10223  frecfzen2  10227  seq3val  10258  seqvalcd  10259  seqf  10261  seq3p1  10262  seqovcd  10263  seqp1cd  10266  monoord  10276  iseqf1olemqcl  10286  iseqf1olemnab  10288  iseqf1olemmo  10292  iseqf1olemqk  10294  seq3f1olemqsumkj  10298  seq3f1olemstep  10301  expnnval  10323  expnegap0  10328  rpexpcl  10339  expnegzap  10354  expgt1  10358  mulexpzap  10360  exprecap  10361  expaddzaplem  10363  expaddzap  10364  expmul  10365  expmulzap  10366  expdivap  10371  ltexp2a  10372  leexp2a  10373  leexp2r  10374  leexp1a  10375  bernneq2  10440  bernneq3  10441  expnbnd  10442  expnlbnd  10443  expnlbnd2  10444  expaddd  10453  expmuld  10454  expclzapd  10456  expap0d  10457  expnegapd  10458  exprecapd  10459  expp1zapd  10460  expm1apd  10461  sqdivapd  10464  mulexpd  10466  expge0d  10469  expge1d  10470  sqoddm1div8  10471  reexpclzapd  10476  leexp2ad  10480  facwordi  10514  faclbnd3  10517  facavg  10520  bcval  10523  bccmpl  10528  bc0k  10530  bcval5  10537  bcpasc  10540  hashfiv01gt1  10556  hashunlem  10578  hashunsng  10581  fiprsshashgt1  10591  hashdifsn  10593  hashdifpr  10594  hashfz  10595  hashxp  10600  hashfacen  10607  zfz1isolemiso  10610  zfz1isolem1  10611  zfz1iso  10612  shftfvalg  10618  seq3shft  10638  mulreap  10664  cjreb  10666  cjap  10706  cnrecnv  10710  cjdivapd  10768  redivapd  10774  imdivapd  10775  resqrexlemdecn  10812  absexpzap  10880  abslt  10888  absle  10889  elicc4abs  10894  abs3lem  10911  fzomaxdiflem  10912  cau3lem  10914  amgm2  10918  abssubge0d  10976  abssuble0d  10977  absdifltd  10978  absdifled  10979  absdivapd  10995  abs3difd  11000  qdenre  11002  maxabslemlub  11007  rexanre  11020  rexico  11021  fimaxre2  11026  lemininf  11033  ltmininf  11034  rpmincl  11037  mul0inf  11040  xrmaxiflemlub  11045  xrmaxltsup  11055  xrmaxaddlem  11057  xrmaxadd  11058  xrltmininf  11067  xrlemininf  11068  xrminltinf  11069  xrminadd  11072  xrbdtri  11073  climshftlemg  11099  climshft2  11103  addcn2  11107  mulcn2  11109  reccn2ap  11110  cn1lem  11111  climadd  11123  climmul  11124  climsub  11125  climsqz  11132  climsqz2  11133  climrecvg1n  11145  climcvg1nlem  11146  fisumss  11189  fsumsplitsn  11207  sumpr  11210  fsumsplitsnun  11216  fsum2dlemstep  11231  fisumcom2  11235  fisum0diag2  11244  fsumconst  11251  modfsummodlemstep  11254  fsumlessfi  11257  fsumabs  11262  fsumiun  11274  hashiun  11275  hash2iun  11276  hash2iun1dif1  11277  binomlem  11280  bcxmas  11286  isumshft  11287  isumlessdc  11293  expcnvap0  11299  expcnvre  11300  geosergap  11303  cvgratnnlembern  11320  cvgratnnlemnexp  11321  cvgratnnlemmn  11322  mertenslemi1  11332  efaddlem  11408  eftlub  11424  efltim  11432  eirraplem  11510  dvdsval3  11524  nndivdvds  11526  summodnegmod  11551  modmulconst  11552  dvds2subd  11556  dvdsmultr1d  11559  dvdsmultr2  11560  dvdsabseq  11572  dvdsfac  11585  dvdsmod  11587  oddge22np1  11605  ltoddhalfle  11617  halfleoddlt  11618  nn0ehalf  11627  nno  11630  nn0oddm1d2  11633  divalglemnn  11642  divalg  11648  divalgmod  11651  fldivndvdslt  11659  flodddiv4lt  11660  flodddiv4t2lthalf  11661  infssuzex  11669  dvdsbnd  11672  gcdneg  11697  gcdaddm  11699  modgcd  11706  gcdmultipled  11708  dvdsgcdidd  11709  bezoutlemnewy  11711  bezoutlemstep  11712  bezoutlembi  11720  dvdsgcdb  11728  gcdass  11730  mulgcd  11731  dvdsmulgcd  11740  rpmulgcd  11741  sqgcd  11744  nn0seqcvgd  11749  eucalglt  11765  gcddvdslcm  11781  lcmgcdlem  11785  lcmdvdsb  11792  lcmass  11793  ncoprmgcdne1b  11797  coprmdvds2  11801  mulgcddvds  11802  rpmulgcd2  11803  qredeu  11805  rpdvds  11807  divgcdcoprm0  11809  cncongr1  11811  cncongr2  11812  isprm2lem  11824  prmind2  11828  nprm  11831  dvdsnprmd  11833  exprmfct  11845  prmdvdsfz  11846  divgcdodd  11848  isprm6  11852  prmdvdsexp  11853  prmexpb  11856  prmfac1  11857  rpexp  11858  rpexp12i  11860  pw2dvdseulemle  11872  sqpweven  11880  2sqpwodd  11881  divnumden  11901  numdensq  11907  nonsq  11912  hashdvds  11924  phiprmpw  11925  crth  11927  phimullem  11928  hashgcdlem  11930  ennnfonelemp1  11946  ennnfonelemex  11954  ennnfonelemrn  11959  ctinfom  11968  ctiunct  11980  strsetsid  12022  fvsetsid  12023  setsabsd  12028  setscom  12029  ressid2  12048  ressval2  12049  srngstrd  12111  lmodstrd  12122  ipsstrd  12130  topgrpstrd  12140  difopn  12307  uncld  12312  ntrin  12323  clsss2  12328  ntrcls0  12330  topssnei  12361  neissex  12364  restbasg  12367  tgrest  12368  resttopon  12370  restabs  12374  restopnb  12380  cnpfval  12394  cnprcl2k  12405  tgcnp  12408  iscnp4  12417  cnpnei  12418  cnptopco  12421  cncnpi  12427  cncnp  12429  cnconst2  12432  cnrest  12434  cnrest2  12435  cnrest2r  12436  cnptopresti  12437  cnptoprest  12438  cnptoprest2  12439  lmss  12445  lmtopcnp  12449  txvalex  12453  txval  12454  txbasval  12466  txcnp  12470  txcnmpt  12472  txcn  12474  txdis1cn  12477  lmcn2  12479  cnmptc  12481  cnmpt11  12482  cnmpt1t  12484  cnmpt12  12486  cnmpt21  12490  cnmpt2t  12492  cnmpt22  12493  cnmpt22f  12494  cnmptcom  12497  hmeores  12514  txhmeo  12518  psmettri  12529  xmettri  12571  metrtri  12576  xmetres2  12578  blfvalps  12584  bldisj  12600  blgt0  12601  xblss2ps  12603  xblss2  12604  blhalf  12607  blininf  12623  blssps  12626  blss  12627  blssexps  12628  blssex  12629  blin2  12631  xmeter  12635  blnei  12691  blsscls2  12692  metss2lem  12696  bdmetval  12699  bdxmet  12700  bdbl  12702  xmetxp  12706  xmetxpbl  12707  xmettxlem  12708  xmettx  12709  metcnp3  12710  metcnp  12711  metcnp2  12712  metcnpi  12714  metcnpi2  12715  metcnpi3  12716  txmetcnp  12717  metcnpd  12719  tgqioo  12746  addcncntoplem  12750  fsumcncntop  12755  mulc1cncf  12775  cncfco  12777  mulcncflem  12789  mulcncf  12790  suplociccreex  12801  suplociccex  12802  dedekindicc  12810  ivthinclemlm  12811  ivthinclemum  12812  ivthinclemlopn  12813  ivthinclemuopn  12815  ivthinclemloc  12818  ivthdec  12821  limccl  12827  ellimc3apf  12828  limcimolemlt  12832  cnplimclemle  12836  cnplimclemr  12837  limccnpcntop  12843  limccnp2lem  12844  limccnp2cntop  12845  reldvg  12847  eldvap  12850  dvbssntrcntop  12852  dvcnp2cntop  12862  dvmulxxbr  12865  dvrecap  12876  dveflem  12886  reeff1o  12893  efltlemlt  12894  sin0pilem2  12902  ptolemy  12944  sinq12gt0  12950  cxprec  13030  rpcxproot  13033  cxpmuld  13055  rpabscxpbnd  13058  rplogbval  13061  rplogbchbase  13066  relogbval  13067  relogbzcl  13068  rplogbreexp  13069  rprelogbmul  13071  rprelogbdiv  13073  nnlogbexp  13075  relogbcxpbap  13081  logbgt0b  13082  logbgcd1irr  13083  logbgcd1irraplemexp  13084  logbgcd1irraplemap  13085  apdifflemr  13398  apdiff  13399
  Copyright terms: Public domain W3C validator