Theorem syl12anc 850

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 521	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 596	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl22anc  852  raaan  4473  raaanv  4474  raaan2  4477  copsex2dv  5465  soltmin  6129  xpdifid  6158  xpdifcnvepel  6159  reuop  6296  f1dom3fv3dif  7272  f1prex  7292  cocan1  7299  fliftfun  7320  soisores  7335  soisoi  7336  isopolem  7353  f1oiso2  7360  weniso  7364  caovcld  7614  caovcomd  7617  onminex  7816  fnwe2lem4  8148  poxp2  8160  poxp3  8167  poseq  8175  tfrlem12  8397  omeulem1  8590  nnaordex2  8648  oaabs2  8658  omabs  8660  eldifsucnn  8673  naddcllem  8685  erov  8835  findcard2d  9182  frfi  9276  finsschain  9348  suplub2  9453  supgtoreq  9463  supisolem  9466  ordiso2  9509  ordtypelem7  9518  wemaplem2  9541  wemapsolem  9544  cantnflt  9673  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  wemapwe  9698  cnfcomlem  9700  cnfcom  9701  cnfcom3lem  9704  infxpenlem  10092  fseqenlem1  10103  dfac12lem2  10223  infpssrlem4  10384  enfin2i  10399  isf34lem7  10457  isf34lem6  10458  fin1a2lem7  10484  fin1a2lem10  10487  fin1a2lem11  10488  fin1a2lem13  10490  ttukeylem6  10592  ttukeylem7  10593  iundom2g  10624  fpwwe2lem5  10720  fpwwe2lem6  10721  fpwwe2lem8  10723  fpwwe2lem11  10726  fpwwe2  10728  canthnumlem  10733  canthwelem  10735  canthp1lem2  10738  pwfseqlem4  10747  inar1  10860  intgru  10899  distrlem4pr  11111  conjmul  12034  lediv12a  12210  recp1lt1  12215  cju  12316  gtndiv  12776  zsupss  13064  uzsupss  13067  icc0  13524  iccssioo2  13550  fzrev3  13724  ico01fl0  13959  fldiv  14000  modabs  14044  modltm1p1mod  14066  modifeq2int  14076  modsumfzodifsn  14087  seqcaopr  14182  seqf1olem1  14184  seqof2  14203  crreczi  14372  seqcoll  14609  seqcoll2  14610  hashtpg  14630  swrdccat3b  14889  sgnmul  15260  01sqrexlem2  15410  resqrex  15417  abs1m  15503  isercoll  15835  zsum  15884  fsum2dlem  15936  fsumcom2  15940  fprod2dlem  16147  fprodcom2  16151  efsub  16268  bitsinv2  16613  sqgcd  16736  expgcd  16737  qredeu  16833  isprm7  16884  pcpremul  17021  pceulem  17023  pczpre  17025  pcdiv  17030  pcqmul  17031  pcqdiv  17035  pcexp  17037  pcdvdsb  17047  pcneg  17052  pcdvdstr  17054  pcgcd1  17055  pc2dvds  17057  pcz  17059  pcaddlem  17066  pcadd  17067  qexpz  17079  expnprm  17080  infpnlem2  17089  ramub2  17192  ramub1lem1  17204  setsstruct2  17352  f1ocpbllem  17696  f1ovscpbl  17698  mreexexlem3d  17820  mreexexlem4d  17821  fthi  18095  ipodrsima  18715  chnind  18795  mgmpropd  18829  sgrppropd  18920  mndpropd  18951  grpsubpropd2  19256  f1ghm0to0  19459  ghmqusker  19501  symgfvne  19595  f1omvdmvd  19657  f1otrspeq  19661  pmtrdifwrdel  19699  pmtrdifwrdel2  19700  psgnunilem2  19709  psgnunilem3  19710  psgnvalii  19723  odf1  19776  lsmpropd  19891  ablnnncan  20036  gsummptshft  20150  dprdf1o  20248  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfaclem1  20297  ablfaclem2  20302  rngpropd  20396  srgbinomlem3  20454  ringpropd  20519  orngsqr  21123  ornglmullt  21126  orngrmullt  21127  lmodprop2d  21199  lsspropd  21292  lmhmpropd  21348  lbspropd  21374  lbsextlem3  21438  unichnlidl  21516  ssdifidllem  21640  iporthcom  21941  obslbs  22036  assapropd  22179  psrass1  22271  psrass23l  22274  psrass23  22276  mplsubrg  22312  mplmon  22344  mplmonmul  22345  mplcoe1  22346  mplbas2  22351  mplind  22379  evlslem2  22388  mpfind  22424  gsumply1subr  22551  psrplusgpropd  22553  ply1scln0  22610  evls1addd  22689  evls1muld  22690  evls1vsca  22691  asclply1subcl  22692  scmataddcl  22831  scmatsubcl  22832  scmatmulcl  22833  smatvscl  22839  scmatrhmcl  22843  mat1scmat  22854  smadiadetglem2  22987  cramerimplem2  23002  cramerimplem3  23003  cramerimp  23004  1pmatscmul  23020  mat2pmatf1  23047  pm2mp  23143  chmatcl  23146  chmatval  23147  chmaidscmat  23166  chfacfisf  23172  cayhamlem1  23184  cpmidgsumm2pm  23187  cpmidpmat  23191  cpmadugsumfi  23195  cpmadumatpoly  23201  cayhamlem3  23205  pptbas  23326  elcls  23391  neiint  23422  neiptopnei  23450  restbas  23476  neitr  23498  iscnp4  23581  cnconst2  23601  cnpdis  23611  cnt0  23664  cnhaus  23672  cmpcovf  23709  hauscmplem  23724  conncompid  23749  2ndci  23766  2ndc1stc  23769  1stcrest  23771  2ndcctbss  23774  2ndcomap  23777  2ndcsep  23778  dis2ndc  23779  restlly  23802  islly2  23803  lly1stc  23815  dislly  23816  finlocfin  23839  dissnlocfin  23848  locfindis  23849  llycmpkgen2  23869  ptbasfi  23900  neitx  23926  ptpjopn  23931  ptcnplem  23940  upxp  23942  txlly  23955  txtube  23959  tx1stc  23969  txkgen  23971  xkococnlem  23978  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  hmeoimaf1o  24089  reghmph  24112  nrmhmph  24113  ordthmeolem  24120  trfil2  24206  fmfnfm  24277  hauspwpwf1  24306  fclsfnflim  24346  cnextf  24385  cnextcn  24386  tmdgsum2  24415  symgtgp  24425  subgntr  24426  opnsubg  24427  ghmcnp  24434  qustgpopn  24439  tsmsf1o  24464  tsmsxplem1  24472  tsmsxplem2  24473  tsmsxp  24474  ustexsym  24535  restutop  24556  imasdsf1olem  24692  blssexps  24745  blssex  24746  ssblex  24747  imasf1oxms  24808  blcld  24824  stdbdmopn  24837  met1stc  24840  met2ndci  24841  prdsxmslem2  24848  metcnp3  24859  cfilucfil  24878  ngptgp  24955  tgioo  25115  tgqioo  25119  zdis  25136  iccpnfhmeo  25266  xrhmeo  25267  cnheibor  25276  elpi1i  25367  cmetcusp  25675  bncssbn  25695  pjthlem2  25759  ivthlem2  25773  ovolicc1  25837  ovolicc2lem3  25840  ovolicc2lem4  25841  volsup  25877  volivth  25928  vitalilem3  25931  mbflimsup  25987  mbfi1fseqlem1  26036  mbfi1fseqlem3  26038  mbfi1fseqlem5  26040  limcnlp  26198  limcflf  26201  limciun  26214  dvmptfsum  26295  dvcnvlem  26296  dvcvx  26340  facth1  26485  elply2  26514  plypf1  26531  coeeq  26546  aaliou3lem8  26672  ulm2  26712  mtestbdd  26732  reeff1o  26774  logbgcd1irr  27122  dcubic2  27172  quart  27189  xrlimcnp  27296  amgm  27318  harmonicbnd4  27338  perfect  27558  dchrptlem1  27591  bposlem2  27612  lgsfcl2  27630  lgsdir  27659  lgsdi  27661  lgsne0  27662  2lgslem1a1  27716  2sqmod  27763  dchrvmasumlem2  27825  chpdifbndlem2  27881  pntpbnd1  27913  pntpbnd2  27914  padicabv  27957  ltsres  28019  nolesgn2o  28028  nogesgn1o  28030  nodense  28049  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd2lem1  28072  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2lem1  28087  noetalem1  28098  nocvxmin  28141  noeta2  28147  oncutlt  28650  eucliddivs  28762  readdscl  28885  tgcgrxfr  28981  idmot  29000  legid  29050  btwnleg  29051  leg0  29055  tghilberti1  29105  mirreu3  29126  colperpex  29209  lnopp2hpgb  29241  dfprlng2  29425  axcgrrflx  29492  axsegconlem1  29495  axcontlem2  29543  axcontlem12  29553  eengtrkg  29564  wwlksnredwwlkn  30484  0wlkon  30711  0trlon  30715  upgr3v3e3cycl  30781  frgrogt3nreg  30998  nvpi  31269  nmlno0lem  31395  fh1  32220  fh2  32221  nmlnop0iALT  32597  nmopun  32616  branmfn  32707  opsqrlem1  32742  opsqrlem6  32747  mdslmd1lem1  32927  csmdsymi  32936  atom1d  32955  chirredlem2  32993  cdj1i  33035  cdj3i  33043  fcnvgreu  33266  suppovss  33274  xrofsup  33359  nn0difffzod  33396  pwrssmgc  33561  gsummpt2d  33610  gsumhashmul  33628  odpmco  33647  cycpmco2lem6  33692  cycpmco2  33694  cyc3evpm  33711  cycpmconjslem2  33716  fxpsubg  33734  fxpsdrg  33736  archirngz  33750  archiabllem2a  33755  elrgspnlem4  33806  rloc0g  33833  rloc1r  33834  domnpropd  33841  sdrgdvcl  33861  sdrginvcl  33862  lindssn  33933  lindfpropd  33937  ssmxidllem  33998  drnglring  34024  dflring2  34025  rsprprmprmidlb  34055  rprmirredb  34064  1arithufd  34080  ply1asclunit  34106  ply1dg1rt  34112  ply1dg3rt0irred  34116  ply1degltel  34126  ply1degleel  34127  ply1degltlss  34128  psrmonmul  34182  esplyind  34207  esplyindfv  34208  lsssra  34220  lindsun  34257  dimkerim  34259  fedgmullem2  34262  fldextrspunlem1  34307  fldextrspunfld  34308  irngss  34319  irngnzply1  34323  algextdeglem2  34350  algextdeglem4  34352  constrext2chnlem  34382  metideq  34525  metider  34526  pstmfval  34528  lmxrge0  34584  qqhval2  34614  qqhf  34618  qqhghm  34620  qqhrhm  34621  esumpcvgval  34710  esum2dlem  34724  esum2d  34725  sigainb  34769  insiga  34770  ddemeas  34869  imambfm  34894  dya2icoseg  34909  dya2iocnrect  34913  eulerpartlemgvv  35008  probun  35051  ballotlemfc0  35125  ballotlemfcc  35126  breprexplemc  35261  erdszelem8  35963  erdszelem9  35964  erdsze2lem2  35969  cnpconn  35995  txpconn  35997  ptpconn  35998  indispconn  35999  connpconn  36000  cvxpconn  36007  cnllysconn  36010  cvmcov2  36040  cvmopnlem  36043  cvmliftmolem1  36046  cvmliftlem14  36062  cvmliftlem15  36063  cvmlift2lem13  36080  cvmlift3lem2  36085  cvmlift3lem9  36092  seglerflx  36877  seglemin  36878  btwnsegle  36882  hilbert1.1  36919  neibastop2lem  37148  weiunfrlem  37252  weiunso  37254  mh-inf3f1  37329  bj-finsumval0  38207  qdiff  38249  relowlssretop  38287  wl-2sb6d  38491  tan2h  38536  poimirlem1  38540  poimirlem3  38542  poimirlem4  38543  poimirlem9  38548  poimirlem22  38561  poimirlem28  38567  heicant  38574  mblfinlem2  38577  itg2addnc  38593  ftc2nc  38621  dvasin  38623  sdclem1  38678  fdc  38680  istotbnd3  38706  sstotbnd  38710  prdstotbnd  38729  prdsbnd2  38730  cntotbnd  38731  rngoisocnv  38916  lsmsat  40066  islfld  40120  ps-2  40536  lplnexllnN  40622  4atlem9  40661  4atlem10a  40662  lnatexN  40837  2lnat  40842  pmapjat1  40911  lhpj1  41080  lhpm0atN  41087  4atexlemex2  41129  4atex  41134  4atex2-0aOLDN  41136  4atex2-0cOLDN  41138  lautcnvle  41147  lautj  41151  lautm  41152  idltrn  41208  cdleme01N  41279  cdleme0ex1N  41281  cdleme5  41298  cdleme9  41311  cdleme11c  41319  cdleme11g  41323  cdlemefrs29bpre0  41454  cdlemefrs29cpre1  41456  cdlemefrs32fva1  41459  cdleme32fva  41495  cdleme32fva1  41496  cdleme32fvaw  41497  cdleme32d  41502  cdleme32f  41504  cdleme35fnpq  41507  cdleme48d  41593  cdleme48gfv  41595  cdleme50ltrn  41615  trlord  41627  cdlemg4b1  41667  cdlemg4b2  41668  cdlemg13a  41709  cdlemg17a  41719  cdlemg17f  41724  erng1lem  42045  erngdvlem3  42048  erngdvlem4  42049  erng1r  42053  erngdvlem3-rN  42056  erngdvlem4-rN  42057  dva0g  42085  dialss  42104  dia0  42110  dia1N  42111  diaglbN  42113  diameetN  42114  diainN  42115  diaintclN  42116  dia1dim  42119  dia2dimlem5  42126  dia2dimlem7  42128  dia2dimlem9  42130  dia2dimlem10  42131  dia2dimlem12  42133  dia2dimlem13  42134  dvhopvadd  42151  dvhvaddass  42155  dvhopvsca  42160  tendolinv  42163  tendorinv  42164  dvhlveclem  42166  dvh0g  42169  dvheveccl  42170  dvhopN  42174  docaclN  42182  diaocN  42183  djajN  42195  dib0  42222  dib1dim  42223  dibglbN  42224  dibintclN  42225  dib1dim2  42226  diblss  42228  diblsmopel  42229  dicvaddcl  42248  dicvscacl  42249  diclspsn  42252  cdlemn4a  42257  cdlemn11c  42267  dihjustlem  42274  dihord1  42276  dihord2a  42277  dihord2b  42278  dihord2cN  42279  dihord11b  42280  dihord11c  42282  dihord2pre  42283  dihlsscpre  42292  dih1dimb  42298  dib2dim  42301  dih2dimb  42302  dih2dimbALTN  42303  dihvalcq2  42305  dihopelvalcpre  42306  dihord6apre  42314  dihord5b  42317  dihord5apre  42320  dih0  42338  dihmeetlem1N  42348  dihglblem5apreN  42349  dihglblem3N  42353  dihmeetlem2N  42357  dihglbcpreN  42358  dihmeetlem4preN  42364  dih1dimatlem0  42386  dih1dimatlem  42387  dihatlat  42392  dihatexv  42396  dihglb2  42400  dihmeet  42401  dihintcl  42402  dihmeet2  42404  doch2val2  42422  dochocss  42424  dihoml4c  42434  dochdmj1  42448  djhlj  42459  djhljjN  42460  djhjlj  42461  dihsumssj  42466  djhexmid  42469  djhlsmcl  42472  djhcvat42  42473  dihjatcclem4  42479  dihjat1lem  42486  dihsmsprn  42488  dihjat3  42490  dvh3dim2  42506  dvh3dim3N  42507  dochkr1OLDN  42537  lclkrlem2c  42567  lclkrlem2d  42568  mapdpglem23  42752  hdmap11lem2  42900  0prjspn  43665  mzpcompact2lem  43762  diophrw  43770  rexrabdioph  43801  eldioph4b  43818  pellexlem5  43840  pellfund14  43905  acongtr  43985  gicabl  44101  hbtlem2  44126  hbtlem4  44128  hbtlem5  44130  dgraalem  44147  aaitgo  44164  onexlimgt  44245  onexoegt  44246  oalim2cl  44291  cantnfresb  44326  onmcl  44333  tfsconcatfv  44343  tfsconcatrn  44344  ofoaid1  44360  ofoaid2  44361  ntrclsk13  45071  gneispb  45131  wessf1ornlem  46200  ltdiv23neg  46405  islptre  46631  limclner  46661  icccncfext  46897  stoweidlem1  47011  stoweidlem14  47024  stoweidlem24  47034  stoweidlem46  47056  stoweidlem57  47067  dirkercncflem2  47114  fourierdlem20  47137  fourierdlem41  47158  fourierdlem46  47162  fourierdlem48  47164  fourierdlem50  47166  fourierdlem62  47178  fourierdlem63  47179  fourierdlem64  47180  fourierdlem65  47181  fourierdlem76  47192  fourierdlem79  47195  fourierdlem103  47219  fourierdlem104  47220  etransclem47  47291  m1modmmod  48434  iccpartiun  48516  reupr  48604  sqrtpwpw2p  48623  fmtnoprmfac1lem  48649  fmtnoprmfac2lem1  48651  lighneallem4a  48693  requad2  48721  perfectALTV  48821  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  isuspgrim0lem  48991  isuspgrim0  48992  isuspgrimlem  48993  upgrimwlklem2  48996  upgrimwlklem3  48997  upgrimtrlslem1  49002  uhgrimisgrgriclem  49028  uhgrimisgrgric  49029  clnbgrgrimlem  49031  grimgrtri  49047  gpgedgvtx1  49160  gpgedg2ov  49164  gpgedg2iv  49165  gsumlsscl  49492  lincsumcl  49543  lincscmcl  49544  isldepslvec2  49597  elbigo2  49664  relogbdivb  49674  blennnt2  49701  dignn0ldlem  49714  itsclc0yqsollem2  49875  inlinecirc02p  49899  lubeldm2  50064  glbeldm2  50065  lubsscl  50068  glbsscl  50069  isclatd  50091  sectpropdlem  50144  invpropdlem  50146  isopropdlem  50148  uptrlem1  50318  fucofulem1  50418  fullthinc  50558