Theorem syl3anc 1228

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

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1167	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl111anc.4	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 968

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 970

This theorem is referenced by:  syl112anc  1232  syl121anc  1233  syl211anc  1234  syl113anc  1240  syl131anc  1241  syl311anc  1242  syld3an3  1273  3jaod  1294  mpd3an23  1329  stoic4a  1420  rspc3ev  2846  sbciedf  2985  euotd  4231  ordelord  4358  wetriext  4553  releldm  4838  relelrn  4839  f1imass  5741  ovmpodxf  5963  ovmpodf  5969  fovrnd  5982  offval  6056  caoftrn  6074  offval3  6099  fnmpoovd  6179  tfrlemisucaccv  6289  tfrlemiubacc  6294  tfr1onlemsucaccv  6305  tfr1onlembfn  6308  tfrcllemsucaccv  6318  tfrcllembfn  6321  rdgss  6347  rdgisuc1  6348  rdgisucinc  6349  frecrdg  6372  mapsspm  6644  en2d  6730  en3d  6731  dom3d  6736  ssdomg  6740  f1imaen2g  6755  2dom  6767  cnven  6770  mapen  6808  mapxpen  6810  phpelm  6828  fidifsnen  6832  dif1en  6841  dif1enen  6842  diffisn  6855  isinfinf  6859  unfidisj  6883  unfiin  6887  tpfidisj  6889  xpfi  6891  fisseneq  6893  phpeqd  6894  ssfirab  6895  fnfi  6898  f1dmvrnfibi  6905  iunfidisj  6907  f1finf1o  6908  en1eqsn  6909  fidcenumlemr  6916  updjudhcoinlf  7041  updjudhcoinrg  7042  difinfinf  7062  en2eleq  7147  en2other2  7148  dju1en  7165  djuassen  7169  xpdjuen  7170  addcmpblnq  7304  addassnqg  7319  distrnqg  7324  ltsonq  7335  ltanqg  7337  ltmnqg  7338  ltaddnq  7344  ltexnqq  7345  prarloclemarch  7355  ltrnqg  7357  addcmpblnq0  7380  nnanq0  7395  distrnq0  7396  addassnq0  7399  prarloclemlt  7430  prarloclemcalc  7439  addnqprllem  7464  addnqprulem  7465  addnqprl  7466  addnqpru  7467  addlocprlemgt  7471  appdivnq  7500  prmuloclemcalc  7502  mulnqprl  7505  mulnqpru  7506  mullocprlem  7507  distrlem4prl  7521  distrlem4pru  7522  ltprordil  7526  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  ltaprlem  7555  ltaprg  7556  addextpr  7558  recexprlem1ssu  7571  aptipr  7578  ltmprr  7579  caucvgprlemcanl  7581  cauappcvgprlemopl  7583  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprprlemloccalc  7621  caucvgprprlemml  7631  caucvgprprlemopl  7634  caucvgprprlemloc  7640  caucvgprprlemexb  7644  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  suplocexprlemmu  7655  suplocexprlemru  7656  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  ltsrprg  7684  distrsrg  7696  lttrsr  7699  ltsosr  7701  1idsr  7705  ltasrg  7707  recexgt0sr  7710  mulgt0sr  7715  mulextsr1lem  7717  srpospr  7720  prsradd  7723  prsrlt  7724  caucvgsrlemoffval  7733  caucvgsrlemoffgt1  7736  caucvgsrlemoffres  7737  caucvgsr  7739  ltpsrprg  7740  map2psrprg  7742  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  pitoregt0  7786  recidpirqlemcalc  7794  axmulass  7810  axdistr  7811  rereceu  7826  recriota  7827  addassd  7917  mulassd  7918  adddid  7919  adddird  7920  lelttr  7983  letrd  8018  lelttrd  8019  lttrd  8020  mul12d  8046  mul32d  8047  mul31d  8048  add12d  8061  add32d  8062  cnegexlem3  8071  addcand  8078  addcan2d  8079  pncan  8100  pncan3  8102  subcan2  8119  subsub2  8122  subsub4  8127  npncan3  8132  pnpcan  8133  pnncan  8135  addsub4  8137  subaddd  8223  subadd2d  8224  addsubassd  8225  addsubd  8226  subadd23d  8227  addsub12d  8228  npncand  8229  nppcand  8230  nppcan2d  8231  nppcan3d  8232  subsubd  8233  subsub2d  8234  subsub3d  8235  subsub4d  8236  sub32d  8237  nnncand  8238  nnncan1d  8239  nnncan2d  8240  npncan3d  8241  pnpcand  8242  pnpcan2d  8243  pnncand  8244  ppncand  8245  subcand  8246  subcan2d  8247  subcanad  8248  subcan2ad  8250  subdid  8308  subdird  8309  ltadd2  8313  ltadd2d  8315  ltletrd  8317  ltsubadd  8326  lesubadd  8328  ltaddsub  8330  leaddsub  8332  le2add  8338  lt2add  8339  ltleadd  8340  lesub1  8350  lesub2  8351  ltsub1  8352  ltsub2  8353  lt2sub  8354  le2sub  8355  subge0  8369  lesub0  8373  ltadd1d  8432  leadd1d  8433  leadd2d  8434  ltsubaddd  8435  lesubaddd  8436  ltsubadd2d  8437  lesubadd2d  8438  ltaddsubd  8439  ltaddsub2d  8440  leaddsub2d  8441  subled  8442  lesubd  8443  ltsub23d  8444  ltsub13d  8445  lesub1d  8446  lesub2d  8447  ltsub1d  8448  ltsub2d  8449  gt0add  8467  apcotr  8501  apadd1  8502  addext  8504  mulext1  8506  mulext  8508  gtapd  8531  leltapd  8533  mulap0  8547  mul0eqap  8563  divvalap  8566  divcanap2  8572  diveqap0  8574  divrecap  8580  divassap  8582  divmulassap  8587  divmulasscomap  8588  divdirap  8589  divcanap3  8590  div11ap  8592  rec11ap  8602  divmuldivap  8604  divdivdivap  8605  divmuleqap  8609  dmdcanap  8614  ddcanap  8618  divadddivap  8619  divsubdivap  8620  redivclap  8623  apmul1  8680  divclapd  8682  divcanap1d  8683  divcanap2d  8684  divrecapd  8685  divrecap2d  8686  divcanap3d  8687  divcanap4d  8688  diveqap0d  8689  diveqap1d  8690  diveqap1ad  8691  diveqap0ad  8692  divap0bd  8694  divnegapd  8695  divneg2apd  8696  div2negapd  8697  redivclapd  8727  div2subap  8729  ltmul12a  8751  lemul12b  8752  lt2mul2div  8770  ltdiv2  8778  ltdiv23  8783  avglt1  9091  avglt2  9092  lt2halvesd  9100  div4p1lem1div2  9106  zltp1le  9241  elz2  9258  zdivmul  9277  uztrn  9478  eluzsub  9491  uz3m2nn  9507  qaddcl  9569  elpq  9582  cnref1o  9584  ltdiv2d  9652  lediv2d  9653  divlt1lt  9656  divle1le  9657  ledivge1le  9658  ltmulgt11d  9664  ltmulgt12d  9665  gt0divd  9666  ge0divd  9667  rpgecld  9668  ltmul1d  9670  ltmul2d  9671  lemul1d  9672  lemul2d  9673  ltdiv1d  9674  lediv1d  9675  ltmuldivd  9676  ltmuldiv2d  9677  lemuldivd  9678  lemuldiv2d  9679  ltdivmuld  9680  ltdivmul2d  9681  ledivmuld  9682  ledivmul2d  9683  ltdiv23d  9689  lediv23d  9690  addlelt  9700  xrltso  9728  xrlelttr  9738  xrlttrd  9741  xrlelttrd  9742  xrltletrd  9743  xrletrd  9744  xrre3  9754  xleadd1  9807  xltadd1  9808  xle2add  9811  xlt2add  9812  xlesubadd  9815  xadd4d  9817  ixxss1  9836  ixxss2  9837  ixxss12  9838  iooshf  9884  icoshftf1o  9923  ioodisj  9925  zltaddlt1le  9939  fznlem  9972  fzdifsuc  10012  fzrev  10015  fzrevral2  10037  elfz0fzfz0  10057  elfzmlbp  10063  fzctr  10064  elfzole1  10086  elfzolt2  10087  fzoss2  10103  fzospliti  10107  fzo1fzo0n0  10114  elfzo0z  10115  fzofzim  10119  fzoaddel  10123  eluzgtdifelfzo  10128  elfzodifsumelfzo  10132  ssfzo12bi  10156  elfzonelfzo  10161  fvinim0ffz  10172  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnxr  10189  flqge  10213  2tnp1ge0ge0  10232  intfracq  10251  flqdiv  10252  modqval  10255  modqcld  10259  modqmulnn  10273  zmodcl  10275  zmodfz  10277  modqid  10280  zmodid2  10283  modqabs  10288  modqcyc  10290  modqadd1  10292  modqaddabs  10293  modqaddmod  10294  mulp1mod1  10296  modqmuladd  10297  modqmuladdim  10298  modqmuladdnn0  10299  m1modnnsub1  10301  modqltm1p1mod  10307  modqmul1  10308  modqsubmod  10313  modqsubmodmod  10314  q2txmodxeq0  10315  modaddmodup  10318  modqmulmod  10320  modqaddmulmod  10322  modqdi  10323  modqsubdir  10324  addmodlteq  10329  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  frecfzen2  10358  seq3val  10389  seqvalcd  10390  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  monoord  10407  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemmo  10423  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemstep  10432  expnnval  10454  expnegap0  10459  rpexpcl  10470  expnegzap  10485  expgt1  10489  mulexpzap  10491  exprecap  10492  expaddzaplem  10494  expaddzap  10495  expmul  10496  expmulzap  10497  expdivap  10502  ltexp2a  10503  leexp2a  10504  leexp2r  10505  leexp1a  10506  bernneq2  10572  bernneq3  10573  expnbnd  10574  expnlbnd  10575  expnlbnd2  10576  expaddd  10586  expmuld  10587  expclzapd  10589  expap0d  10590  expnegapd  10591  exprecapd  10592  expp1zapd  10593  expm1apd  10594  sqdivapd  10597  mulexpd  10599  expge0d  10602  expge1d  10603  sqoddm1div8  10604  reexpclzapd  10609  leexp2ad  10613  facwordi  10649  faclbnd3  10652  facavg  10655  bcval  10658  bccmpl  10663  bc0k  10665  bcval5  10672  bcpasc  10675  hashfiv01gt1  10691  hashunlem  10713  hashunsng  10716  fiprsshashgt1  10726  hashdifsn  10728  hashdifpr  10729  hashfz  10730  hashxp  10735  fiubm  10737  hashfacen  10745  zfz1isolemiso  10748  zfz1isolem1  10749  zfz1iso  10750  shftfvalg  10756  seq3shft  10776  mulreap  10802  cjreb  10804  cjap  10844  cnrecnv  10848  cjdivapd  10906  redivapd  10912  imdivapd  10913  resqrexlemdecn  10950  absexpzap  11018  abslt  11026  absle  11027  elicc4abs  11032  abs3lem  11049  fzomaxdiflem  11050  cau3lem  11052  amgm2  11056  abssubge0d  11114  abssuble0d  11115  absdifltd  11116  absdifled  11117  absdivapd  11133  abs3difd  11138  qdenre  11140  maxabslemlub  11145  rexanre  11158  rexico  11159  fimaxre2  11164  lemininf  11171  ltmininf  11172  rpmincl  11175  mul0inf  11178  xrmaxiflemlub  11185  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  xrltmininf  11207  xrlemininf  11208  xrminltinf  11209  xrminadd  11212  xrbdtri  11213  climshftlemg  11239  climshft2  11243  addcn2  11247  mulcn2  11249  reccn2ap  11250  cn1lem  11251  climadd  11263  climmul  11264  climsub  11265  climsqz  11272  climsqz2  11273  climrecvg1n  11285  climcvg1nlem  11286  fisumss  11329  fsumsplitsn  11347  sumpr  11350  fsumsplitsnun  11356  fsum2dlemstep  11371  fisumcom2  11375  fisum0diag2  11384  fsumconst  11391  modfsummodlemstep  11394  fsumlessfi  11397  fsumabs  11402  fsumiun  11414  hashiun  11415  hash2iun  11416  hash2iun1dif1  11417  binomlem  11420  bcxmas  11426  isumshft  11427  isumlessdc  11433  expcnvap0  11439  expcnvre  11440  geosergap  11443  cvgratnnlembern  11460  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  mertenslemi1  11472  fprodssdc  11527  fprodm1  11535  fprodunsn  11541  fprodeq0  11554  fprod2dlemstep  11559  fprodcom2fi  11563  fprodsplitsn  11570  fprodsplit1f  11571  efaddlem  11611  eftlub  11627  efltim  11635  eirraplem  11713  dvdsval3  11727  nndivdvds  11732  modm1div  11736  summodnegmod  11758  modmulconst  11759  dvds2subd  11763  dvds2addd  11765  dvdstrd  11766  dvdsmultr1d  11768  dvdsmultr2  11769  dvdsabseq  11781  dvdsfac  11794  dvdsmod  11796  oddge22np1  11814  ltoddhalfle  11826  halfleoddlt  11827  nn0ehalf  11836  nno  11839  nn0oddm1d2  11842  divalglemnn  11851  divalg  11857  divalgmod  11860  fldivndvdslt  11868  flodddiv4lt  11869  flodddiv4t2lthalf  11870  infssuzex  11878  dvdsbnd  11885  gcdneg  11911  gcdaddm  11913  modgcd  11920  gcdmultipled  11922  dvdsgcdidd  11923  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlembi  11934  dvdsgcdb  11942  gcdass  11944  mulgcd  11945  dvdsmulgcd  11954  rpmulgcd  11955  sqgcd  11958  nnwodc  11965  uzwodc  11966  nn0seqcvgd  11969  eucalglt  11985  gcddvdslcm  12001  lcmgcdlem  12005  lcmdvdsb  12012  lcmass  12013  ncoprmgcdne1b  12017  coprmdvds2  12021  mulgcddvds  12022  rpmulgcd2  12023  qredeu  12025  rpdvds  12027  divgcdcoprm0  12029  cncongr1  12031  cncongr2  12032  isprm2lem  12044  prmind2  12048  nprm  12051  dvdsnprmd  12053  exprmfct  12066  prmdvdsfz  12067  isprm5lem  12069  divgcdodd  12071  isprm6  12075  prmdvdsexp  12076  prmexpb  12079  prmfac1  12080  rpexp  12081  rpexp12i  12083  pw2dvdseulemle  12095  sqpweven  12103  2sqpwodd  12104  divnumden  12124  numdensq  12130  nonsq  12135  hashdvds  12149  phiprmpw  12150  crth  12152  phimullem  12153  eulerthlem1  12155  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  prmdiv  12163  prmdiveq  12164  prmdivdiv  12165  hashgcdlem  12166  phisum  12168  odzdvds  12173  odzphi  12174  vfermltl  12179  powm2modprm  12180  reumodprminv  12181  modprm0  12182  nnnn0modprm0  12183  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem4  12196  pythagtriplem19  12210  pclemub  12215  pcprendvds2  12219  pcpremul  12221  pcval  12224  pcdiv  12230  pcqdiv  12235  pcexp  12237  pcdvdsb  12247  pcidlem  12250  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  pcprmpw2  12260  dvdsprmpweqle  12264  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcmptdvds  12271  fldivp1  12274  pcfaclem  12275  pcfac  12276  pcbc  12277  oddprmdvds  12280  prmpwdvds  12281  pockthlem  12282  pockthg  12283  1arith  12293  4sqlem5  12308  4sqlem6  12309  4sqlem7  12310  4sqlem8  12311  4sqlem9  12312  4sqlem4  12318  ennnfonelemp1  12335  ennnfonelemex  12343  ennnfonelemrn  12348  ctinfom  12357  ctiunct  12369  nninfdclemcl  12377  nninfdclemp1  12379  strsetsid  12423  fvsetsid  12424  setsabsd  12429  setscom  12430  ressid2  12449  ressval2  12450  srngstrd  12512  lmodstrd  12523  ipsstrd  12531  topgrpstrd  12541  difopn  12708  uncld  12713  ntrin  12724  clsss2  12729  ntrcls0  12731  topssnei  12762  neissex  12765  restbasg  12768  tgrest  12769  resttopon  12771  restabs  12775  restopnb  12781  cnpfval  12795  cnprcl2k  12806  tgcnp  12809  iscnp4  12818  cnpnei  12819  cnptopco  12822  cncnpi  12828  cncnp  12830  cnconst2  12833  cnrest  12835  cnrest2  12836  cnrest2r  12837  cnptopresti  12838  cnptoprest  12839  cnptoprest2  12840  lmss  12846  lmtopcnp  12850  txvalex  12854  txval  12855  txbasval  12867  txcnp  12871  txcnmpt  12873  txcn  12875  txdis1cn  12878  lmcn2  12880  cnmptc  12882  cnmpt11  12883  cnmpt1t  12885  cnmpt12  12887  cnmpt21  12891  cnmpt2t  12893  cnmpt22  12894  cnmpt22f  12895  cnmptcom  12898  hmeores  12915  txhmeo  12919  psmettri  12930  xmettri  12972  metrtri  12977  xmetres2  12979  blfvalps  12985  bldisj  13001  blgt0  13002  xblss2ps  13004  xblss2  13005  blhalf  13008  blininf  13024  blssps  13027  blss  13028  blssexps  13029  blssex  13030  blin2  13032  xmeter  13036  blnei  13092  blsscls2  13093  metss2lem  13097  bdmetval  13100  bdxmet  13101  bdbl  13103  xmetxp  13107  xmetxpbl  13108  xmettxlem  13109  xmettx  13110  metcnp3  13111  metcnp  13112  metcnp2  13113  metcnpi  13115  metcnpi2  13116  metcnpi3  13117  txmetcnp  13118  metcnpd  13120  tgqioo  13147  addcncntoplem  13151  fsumcncntop  13156  mulc1cncf  13176  cncfco  13178  mulcncflem  13190  mulcncf  13191  suplociccreex  13202  suplociccex  13203  dedekindicc  13211  ivthinclemlm  13212  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinclemloc  13219  ivthdec  13222  limccl  13228  ellimc3apf  13229  limcimolemlt  13233  cnplimclemle  13237  cnplimclemr  13238  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  reldvg  13248  eldvap  13251  dvbssntrcntop  13253  dvcnp2cntop  13263  dvmulxxbr  13266  dvrecap  13277  dveflem  13287  reeff1o  13294  efltlemlt  13295  sin0pilem2  13303  ptolemy  13345  sinq12gt0  13351  cxprec  13431  rpcxproot  13434  cxpmuld  13456  rpabscxpbnd  13459  rplogbval  13463  rplogbchbase  13468  relogbval  13469  relogbzcl  13470  rplogbreexp  13471  rprelogbmul  13473  rprelogbdiv  13475  nnlogbexp  13477  relogbcxpbap  13483  logbgt0b  13484  logbgcd1irr  13485  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  logbprmirr  13490  lgslem1  13501  lgslem4  13504  lgsval2lem  13511  lgsvalmod  13520  lgsval4a  13523  lgsneg  13525  lgsmod  13527  lgsdirprm  13535  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  2sqlem2  13551  2sqlem3  13553  2sqlem4  13554  2sqlem6  13556  2sqlem8  13559  apdifflemr  13886  apdiff  13887  iswomni0  13890