Theorem syl12anc 836

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl12anc.4	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
syl12anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl12anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 584	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  syl22anc  838  raaan  4492  raaanv  4493  raaan2  4496  copsex2dv  5469  soltmin  6125  xpdifid  6157  reuop  6282  f1dom3fv3dif  7260  f1prex  7276  cocan1  7283  fliftfun  7304  soisores  7319  soisoi  7320  isopolem  7337  f1oiso2  7344  weniso  7346  caovcld  7598  caovcomd  7601  onminex  7794  poxp2  8140  poxp3  8147  poseq  8155  tfrlem12  8401  omeulem1  8592  nnaordex2  8649  oaabs2  8659  omabs  8661  eldifsucnn  8674  naddcllem  8686  erov  8826  findcard2d  9178  frfi  9291  finsschain  9369  suplub2  9471  supgtoreq  9481  supisolem  9484  ordiso2  9527  ordtypelem7  9536  wemaplem2  9559  wemapsolem  9562  cantnflt  9684  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1  9701  wemapwe  9709  cnfcomlem  9711  cnfcom  9712  cnfcom3lem  9715  infxpenlem  10025  fseqenlem1  10036  dfac12lem2  10157  infpssrlem4  10318  enfin2i  10333  isf34lem7  10391  isf34lem6  10392  fin1a2lem7  10418  fin1a2lem10  10421  fin1a2lem11  10422  fin1a2lem13  10424  ttukeylem6  10526  ttukeylem7  10527  iundom2g  10552  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem8  10650  fpwwe2lem11  10653  fpwwe2  10655  canthnumlem  10660  canthwelem  10662  canthp1lem2  10665  pwfseqlem4  10674  inar1  10787  intgru  10826  distrlem4pr  11038  conjmul  11956  lediv12a  12133  recp1lt1  12138  cju  12234  gtndiv  12668  zsupss  12951  uzsupss  12954  icc0  13408  iccssioo2  13434  fzrev3  13605  ico01fl0  13834  fldiv  13875  modabs  13919  modltm1p1mod  13939  modifeq2int  13949  modsumfzodifsn  13960  seqcaopr  14055  seqf1olem1  14057  seqof2  14076  crreczi  14244  seqcoll  14480  seqcoll2  14481  hashtpg  14501  swrdccat3b  14756  01sqrexlem2  15260  resqrex  15267  abs1m  15352  isercoll  15682  zsum  15732  fsum2dlem  15784  fsumcom2  15788  fprod2dlem  15994  fprodcom2  15998  efsub  16116  bitsinv2  16460  sqgcd  16579  expgcd  16580  qredeu  16675  isprm7  16725  pcpremul  16861  pceulem  16863  pczpre  16865  pcdiv  16870  pcqmul  16871  pcqdiv  16875  pcexp  16877  pcdvdsb  16887  pcneg  16892  pcdvdstr  16894  pcgcd1  16895  pc2dvds  16897  pcz  16899  pcaddlem  16906  pcadd  16907  qexpz  16919  expnprm  16920  infpnlem2  16929  ramub2  17032  ramub1lem1  17044  setsstruct2  17191  f1ocpbllem  17536  f1ovscpbl  17538  mreexexlem3d  17656  mreexexlem4d  17657  fthi  17931  ipodrsima  18549  mgmpropd  18627  sgrppropd  18707  mndpropd  18735  grpsubpropd2  19027  f1ghm0to0  19226  ghmqusker  19268  symgfvne  19360  f1omvdmvd  19422  f1otrspeq  19426  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  psgnunilem2  19474  psgnunilem3  19475  psgnvalii  19488  odf1  19541  lsmpropd  19656  ablnnncan  19801  gsummptshft  19915  dprdf1o  20013  pgpfac1lem3  20058  pgpfac1lem5  20060  pgpfaclem1  20062  ablfaclem2  20067  rngpropd  20132  srgbinomlem3  20186  ringpropd  20246  lmodprop2d  20879  lsspropd  20973  lmhmpropd  21029  lbspropd  21055  lbsextlem3  21119  iporthcom  21593  obslbs  21688  assapropd  21830  psrass1  21922  psrass23l  21925  psrass23  21927  mplsubrg  21963  mplmon  21991  mplmonmul  21992  mplcoe1  21993  mplbas2  21998  mplind  22026  evlslem2  22035  mpfind  22063  gsumply1subr  22167  psrplusgpropd  22169  ply1scln0  22227  evls1addd  22307  evls1muld  22308  evls1vsca  22309  asclply1subcl  22310  scmataddcl  22452  scmatsubcl  22453  scmatmulcl  22454  smatvscl  22460  scmatrhmcl  22464  mat1scmat  22475  smadiadetglem2  22608  cramerimplem2  22620  cramerimplem3  22621  cramerimp  22622  1pmatscmul  22638  mat2pmatf1  22665  pm2mp  22761  chmatcl  22764  chmatval  22765  chmaidscmat  22784  chfacfisf  22790  cayhamlem1  22802  cpmidgsumm2pm  22805  cpmidpmat  22809  cpmadugsumfi  22813  cpmadumatpoly  22819  cayhamlem3  22823  pptbas  22944  elcls  23009  neiint  23040  neiptopnei  23068  restbas  23094  neitr  23116  iscnp4  23199  cnconst2  23219  cnpdis  23229  cnt0  23282  cnhaus  23290  cmpcovf  23327  hauscmplem  23342  conncompid  23367  2ndci  23384  2ndc1stc  23387  1stcrest  23389  2ndcctbss  23391  2ndcomap  23394  2ndcsep  23395  dis2ndc  23396  restlly  23419  islly2  23420  lly1stc  23432  dislly  23433  finlocfin  23456  dissnlocfin  23465  locfindis  23466  llycmpkgen2  23486  ptbasfi  23517  neitx  23543  ptpjopn  23548  ptcnplem  23557  upxp  23559  txlly  23572  txtube  23576  tx1stc  23586  txkgen  23588  xkococnlem  23595  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  hmeoimaf1o  23706  reghmph  23729  nrmhmph  23730  ordthmeolem  23737  trfil2  23823  fmfnfm  23894  hauspwpwf1  23923  fclsfnflim  23963  cnextf  24002  cnextcn  24003  tmdgsum2  24032  symgtgp  24042  subgntr  24043  opnsubg  24044  ghmcnp  24051  qustgpopn  24056  tsmsf1o  24081  tsmsxplem1  24089  tsmsxplem2  24090  tsmsxp  24091  ustexsym  24152  restutop  24174  imasdsf1olem  24310  blssexps  24363  blssex  24364  ssblex  24365  imasf1oxms  24426  blcld  24442  stdbdmopn  24455  met1stc  24458  met2ndci  24459  prdsxmslem2  24466  metcnp3  24477  cfilucfil  24496  ngptgp  24573  tgioo  24733  tgqioo  24737  zdis  24754  iccpnfhmeo  24892  xrhmeo  24893  cnheibor  24903  elpi1i  24995  cmetcusp  25304  bncssbn  25324  pjthlem2  25388  ivthlem2  25403  ovolicc1  25467  ovolicc2lem3  25470  ovolicc2lem4  25471  volsup  25507  volivth  25558  vitalilem3  25561  mbflimsup  25617  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem5  25670  limcnlp  25829  limcflf  25832  limciun  25845  dvmptfsum  25929  dvcnvlem  25930  dvcvx  25975  facth1  26122  elply2  26151  plypf1  26167  coeeq  26182  aaliou3lem8  26303  ulm2  26344  mtestbdd  26364  reeff1o  26407  logbgcd1irr  26754  dcubic2  26804  quart  26821  xrlimcnp  26928  amgm  26951  harmonicbnd4  26971  perfect  27192  dchrptlem1  27225  bposlem2  27246  lgsfcl2  27264  lgsdir  27293  lgsdi  27295  lgsne0  27296  2lgslem1a1  27350  2sqmod  27397  dchrvmasumlem2  27459  chpdifbndlem2  27515  pntpbnd1  27547  pntpbnd2  27548  padicabv  27591  sltres  27624  nolesgn2o  27633  nogesgn1o  27635  nodense  27654  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd2lem1  27677  noinfres  27684  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd2lem1  27692  noetalem1  27703  nocvxmin  27740  noeta2  27746  readdscl  28348  tgcgrxfr  28443  idmot  28462  legid  28512  btwnleg  28513  leg0  28517  tghilberti1  28562  mirreu3  28579  colperpex  28658  lnopp2hpgb  28688  axcgrrflx  28839  axsegconlem1  28842  axcontlem2  28890  axcontlem12  28900  eengtrkg  28911  wwlksnredwwlkn  29823  0wlkon  30047  0trlon  30051  upgr3v3e3cycl  30107  frgrogt3nreg  30324  nvpi  30594  nmlno0lem  30720  fh1  31545  fh2  31546  nmlnop0iALT  31922  nmopun  31941  branmfn  32032  opsqrlem1  32067  opsqrlem6  32072  mdslmd1lem1  32252  csmdsymi  32261  atom1d  32280  chirredlem2  32318  cdj1i  32360  cdj3i  32368  fcnvgreu  32597  suppovss  32604  xrofsup  32690  nn0difffzod  32729  sgnmul  32760  pwrssmgc  32926  chnind  32937  gsummpt2d  32989  gsumhashmul  33001  odpmco  33043  cycpmco2lem6  33088  cycpmco2  33090  cyc3evpm  33107  cycpmconjslem2  33112  archirngz  33133  archiabllem2a  33138  elrgspnlem4  33186  rloc0g  33212  rloc1r  33213  domnpropd  33217  sdrgdvcl  33239  sdrginvcl  33240  orngsqr  33272  ornglmullt  33275  orngrmullt  33276  lindssn  33339  lindfpropd  33343  ssdifidllem  33417  ssmxidllem  33434  rsprprmprmidlb  33484  rprmirredb  33493  1arithufd  33509  ply1asclunit  33533  ply1dg1rt  33538  ply1dg3rt0irred  33541  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  lsssra  33574  lindsun  33611  dimkerim  33613  fedgmullem2  33616  fldextrspunlem1  33662  fldextrspunfld  33663  irngss  33674  irngnzply1  33678  algextdeglem2  33698  algextdeglem4  33700  constrext2chnlem  33730  metideq  33870  metider  33871  pstmfval  33873  lmxrge0  33929  qqhval2  33959  qqhf  33963  qqhghm  33965  qqhrhm  33966  esumpcvgval  34055  esum2dlem  34069  esum2d  34070  sigainb  34113  insiga  34114  ddemeas  34213  imambfm  34240  dya2icoseg  34255  dya2iocnrect  34259  eulerpartlemgvv  34354  probun  34397  ballotlemfc0  34471  ballotlemfcc  34472  breprexplemc  34610  erdszelem8  35166  erdszelem9  35167  erdsze2lem2  35172  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cnllysconn  35213  cvmcov2  35243  cvmopnlem  35246  cvmliftmolem1  35249  cvmliftlem14  35265  cvmliftlem15  35266  cvmlift2lem13  35283  cvmlift3lem2  35288  cvmlift3lem9  35295  seglerflx  36076  seglemin  36077  btwnsegle  36081  hilbert1.1  36118  neibastop2lem  36324  weiunfrlem  36428  weiunso  36430  bj-finsumval0  37249  relowlssretop  37327  wl-2sb6d  37522  tan2h  37582  poimirlem1  37591  poimirlem3  37593  poimirlem4  37594  poimirlem9  37599  poimirlem22  37612  poimirlem28  37618  heicant  37625  mblfinlem2  37628  itg2addnc  37644  ftc2nc  37672  dvasin  37674  sdclem1  37713  fdc  37715  istotbnd3  37741  sstotbnd  37745  prdstotbnd  37764  prdsbnd2  37765  cntotbnd  37766  rngoisocnv  37951  lsmsat  38972  islfld  39026  ps-2  39443  lplnexllnN  39529  4atlem9  39568  4atlem10a  39569  lnatexN  39744  2lnat  39749  pmapjat1  39818  lhpj1  39987  lhpm0atN  39994  4atexlemex2  40036  4atex  40041  4atex2-0aOLDN  40043  4atex2-0cOLDN  40045  lautcnvle  40054  lautj  40058  lautm  40059  idltrn  40115  cdleme01N  40186  cdleme0ex1N  40188  cdleme5  40205  cdleme9  40218  cdleme11c  40226  cdleme11g  40230  cdlemefrs29bpre0  40361  cdlemefrs29cpre1  40363  cdlemefrs32fva1  40366  cdleme32fva  40402  cdleme32fva1  40403  cdleme32fvaw  40404  cdleme32d  40409  cdleme32f  40411  cdleme35fnpq  40414  cdleme48d  40500  cdleme48gfv  40502  cdleme50ltrn  40522  trlord  40534  cdlemg4b1  40574  cdlemg4b2  40575  cdlemg13a  40616  cdlemg17a  40626  cdlemg17f  40631  erng1lem  40952  erngdvlem3  40955  erngdvlem4  40956  erng1r  40960  erngdvlem3-rN  40963  erngdvlem4-rN  40964  dva0g  40992  dialss  41011  dia0  41017  dia1N  41018  diaglbN  41020  diameetN  41021  diainN  41022  diaintclN  41023  dia1dim  41026  dia2dimlem5  41033  dia2dimlem7  41035  dia2dimlem9  41037  dia2dimlem10  41038  dia2dimlem12  41040  dia2dimlem13  41041  dvhopvadd  41058  dvhvaddass  41062  dvhopvsca  41067  tendolinv  41070  tendorinv  41071  dvhlveclem  41073  dvh0g  41076  dvheveccl  41077  dvhopN  41081  docaclN  41089  diaocN  41090  djajN  41102  dib0  41129  dib1dim  41130  dibglbN  41131  dibintclN  41132  dib1dim2  41133  diblss  41135  diblsmopel  41136  dicvaddcl  41155  dicvscacl  41156  diclspsn  41159  cdlemn4a  41164  cdlemn11c  41174  dihjustlem  41181  dihord1  41183  dihord2a  41184  dihord2b  41185  dihord2cN  41186  dihord11b  41187  dihord11c  41189  dihord2pre  41190  dihlsscpre  41199  dih1dimb  41205  dib2dim  41208  dih2dimb  41209  dih2dimbALTN  41210  dihvalcq2  41212  dihopelvalcpre  41213  dihord6apre  41221  dihord5b  41224  dihord5apre  41227  dih0  41245  dihmeetlem1N  41255  dihglblem5apreN  41256  dihglblem3N  41260  dihmeetlem2N  41264  dihglbcpreN  41265  dihmeetlem4preN  41271  dih1dimatlem0  41293  dih1dimatlem  41294  dihatlat  41299  dihatexv  41303  dihglb2  41307  dihmeet  41308  dihintcl  41309  dihmeet2  41311  doch2val2  41329  dochocss  41331  dihoml4c  41341  dochdmj1  41355  djhlj  41366  djhljjN  41367  djhjlj  41368  dihsumssj  41373  djhexmid  41376  djhlsmcl  41379  djhcvat42  41380  dihjatcclem4  41386  dihjat1lem  41393  dihsmsprn  41395  dihjat3  41397  dvh3dim2  41413  dvh3dim3N  41414  dochkr1OLDN  41444  lclkrlem2c  41474  lclkrlem2d  41475  mapdpglem23  41659  hdmap11lem2  41807  0prjspn  42598  mzpcompact2lem  42721  diophrw  42729  rexrabdioph  42764  eldioph4b  42781  pellexlem5  42803  pellfund14  42868  acongtr  42949  fnwe2lem3  43023  gicabl  43070  hbtlem2  43095  hbtlem4  43097  hbtlem5  43099  dgraalem  43116  aaitgo  43133  onexlimgt  43214  onexoegt  43215  oalim2cl  43260  cantnfresb  43295  onmcl  43302  tfsconcatfv  43312  tfsconcatrn  43313  ofoaid1  43329  ofoaid2  43330  ntrclsk13  44042  gneispb  44102  wessf1ornlem  45157  ltdiv23neg  45369  islptre  45596  limclner  45628  icccncfext  45864  stoweidlem1  45978  stoweidlem14  45991  stoweidlem24  46001  stoweidlem46  46023  stoweidlem57  46034  dirkercncflem2  46081  fourierdlem20  46104  fourierdlem41  46125  fourierdlem46  46129  fourierdlem48  46131  fourierdlem50  46133  fourierdlem62  46145  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem76  46159  fourierdlem79  46162  fourierdlem103  46186  fourierdlem104  46187  etransclem47  46258  iccpartiun  47396  reupr  47484  sqrtpwpw2p  47500  fmtnoprmfac1lem  47526  fmtnoprmfac2lem1  47528  lighneallem4a  47570  requad2  47585  perfectALTV  47685  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  isuspgrim0lem  47854  isuspgrim0  47855  isuspgrimlem  47856  upgrimwlklem2  47859  upgrimwlklem3  47860  upgrimtrlslem1  47865  uhgrimisgrgriclem  47891  uhgrimisgrgric  47892  clnbgrgrimlem  47894  grimgrtri  47909  gpgedgvtx1  48014  gsumlsscl  48303  lincsumcl  48355  lincscmcl  48356  isldepslvec2  48409  m1modmmod  48449  elbigo2  48480  relogbdivb  48490  blennnt2  48517  dignn0ldlem  48530  itsclc0yqsollem2  48691  inlinecirc02p  48715  lubeldm2  48878  glbeldm2  48879  lubsscl  48882  glbsscl  48883  isclatd  48905  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955  fucofulem1  49169  fullthinc  49284