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 583	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  4540  raaanv  4541  raaan2  4544  soltmin  6168  xpdifid  6199  reuop  6324  f1dom3fv3dif  7305  f1prex  7320  cocan1  7327  fliftfun  7348  soisores  7363  soisoi  7364  isopolem  7381  f1oiso2  7388  weniso  7390  caovcld  7643  caovcomd  7646  onminex  7838  poxp2  8184  poxp3  8191  poseq  8199  tfrlem12  8445  omeulem1  8638  nnaordex2  8695  oaabs2  8705  omabs  8707  eldifsucnn  8720  naddcllem  8732  erov  8872  findcard2d  9232  frfi  9349  finsschain  9429  suplub2  9530  supgtoreq  9539  supisolem  9542  ordiso2  9584  ordtypelem7  9593  wemaplem2  9616  wemapsolem  9619  cantnflt  9741  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  wemapwe  9766  cnfcomlem  9768  cnfcom  9769  cnfcom3lem  9772  infxpenlem  10082  fseqenlem1  10093  dfac12lem2  10214  infpssrlem4  10375  enfin2i  10390  isf34lem7  10448  isf34lem6  10449  fin1a2lem7  10475  fin1a2lem10  10478  fin1a2lem11  10479  fin1a2lem13  10481  ttukeylem6  10583  ttukeylem7  10584  iundom2g  10609  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  fpwwe2lem11  10710  fpwwe2  10712  canthnumlem  10717  canthwelem  10719  canthp1lem2  10722  pwfseqlem4  10731  inar1  10844  intgru  10883  distrlem4pr  11095  conjmul  12011  lediv12a  12188  recp1lt1  12193  cju  12289  gtndiv  12720  zsupss  13002  uzsupss  13005  icc0  13455  iccssioo2  13480  fzrev3  13650  ico01fl0  13870  fldiv  13911  modabs  13955  modltm1p1mod  13974  modifeq2int  13984  modsumfzodifsn  13995  seqcaopr  14090  seqf1olem1  14092  seqof2  14111  crreczi  14277  seqcoll  14513  seqcoll2  14514  hashtpg  14534  swrdccat3b  14788  01sqrexlem2  15292  resqrex  15299  abs1m  15384  isercoll  15716  zsum  15766  fsum2dlem  15818  fsumcom2  15822  fprod2dlem  16028  fprodcom2  16032  efsub  16148  bitsinv2  16489  sqgcd  16609  expgcd  16610  qredeu  16705  isprm7  16755  pcpremul  16890  pceulem  16892  pczpre  16894  pcdiv  16899  pcqmul  16900  pcqdiv  16904  pcexp  16906  pcdvdsb  16916  pcneg  16921  pcdvdstr  16923  pcgcd1  16924  pc2dvds  16926  pcz  16928  pcaddlem  16935  pcadd  16936  qexpz  16948  expnprm  16949  infpnlem2  16958  ramub2  17061  ramub1lem1  17073  setsstruct2  17221  f1ocpbllem  17584  f1ovscpbl  17586  mreexexlem3d  17704  mreexexlem4d  17705  fthi  17985  ipodrsima  18611  mgmpropd  18689  sgrppropd  18769  mndpropd  18797  grpsubpropd2  19086  f1ghm0to0  19285  ghmqusker  19327  symgfvne  19422  f1omvdmvd  19485  f1otrspeq  19489  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  psgnunilem2  19537  psgnunilem3  19538  psgnvalii  19551  odf1  19604  lsmpropd  19719  ablnnncan  19864  gsummptshft  19978  dprdf1o  20076  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem1  20125  ablfaclem2  20130  rngpropd  20201  srgbinomlem3  20255  ringpropd  20311  lmodprop2d  20944  lsspropd  21039  lmhmpropd  21095  lbspropd  21121  lbsextlem3  21185  iporthcom  21676  obslbs  21773  assapropd  21915  psrass1  22007  psrass23l  22010  psrass23  22012  mplsubrg  22048  mplmon  22076  mplmonmul  22077  mplcoe1  22078  mplbas2  22083  mplind  22117  evlslem2  22126  mpfind  22154  gsumply1subr  22256  psrplusgpropd  22258  ply1scln0  22316  evls1addd  22396  evls1muld  22397  evls1vsca  22398  asclply1subcl  22399  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  smatvscl  22551  scmatrhmcl  22555  mat1scmat  22566  smadiadetglem2  22699  cramerimplem2  22711  cramerimplem3  22712  cramerimp  22713  1pmatscmul  22729  mat2pmatf1  22756  pm2mp  22852  chmatcl  22855  chmatval  22856  chmaidscmat  22875  chfacfisf  22881  cayhamlem1  22893  cpmidgsumm2pm  22896  cpmidpmat  22900  cpmadugsumfi  22904  cpmadumatpoly  22910  cayhamlem3  22914  pptbas  23036  elcls  23102  neiint  23133  neiptopnei  23161  restbas  23187  neitr  23209  iscnp4  23292  cnconst2  23312  cnpdis  23322  cnt0  23375  cnhaus  23383  cmpcovf  23420  hauscmplem  23435  conncompid  23460  2ndci  23477  2ndc1stc  23480  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  dis2ndc  23489  restlly  23512  islly2  23513  lly1stc  23525  dislly  23526  finlocfin  23549  dissnlocfin  23558  locfindis  23559  llycmpkgen2  23579  ptbasfi  23610  neitx  23636  ptpjopn  23641  ptcnplem  23650  upxp  23652  txlly  23665  txtube  23669  tx1stc  23679  txkgen  23681  xkococnlem  23688  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  hmeoimaf1o  23799  reghmph  23822  nrmhmph  23823  ordthmeolem  23830  trfil2  23916  fmfnfm  23987  hauspwpwf1  24016  fclsfnflim  24056  cnextf  24095  cnextcn  24096  tmdgsum2  24125  symgtgp  24135  subgntr  24136  opnsubg  24137  ghmcnp  24144  qustgpopn  24149  tsmsf1o  24174  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  ustexsym  24245  restutop  24267  imasdsf1olem  24404  blssexps  24457  blssex  24458  ssblex  24459  imasf1oxms  24523  blcld  24539  stdbdmopn  24552  met1stc  24555  met2ndci  24556  prdsxmslem2  24563  metcnp3  24574  cfilucfil  24593  ngptgp  24670  tgioo  24837  tgqioo  24841  zdis  24857  iccpnfhmeo  24995  xrhmeo  24996  cnheibor  25006  elpi1i  25098  cmetcusp  25407  bncssbn  25427  pjthlem2  25491  ivthlem2  25506  ovolicc1  25570  ovolicc2lem3  25573  ovolicc2lem4  25574  volsup  25610  volivth  25661  vitalilem3  25664  mbflimsup  25720  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem5  25774  limcnlp  25933  limcflf  25936  limciun  25949  dvmptfsum  26033  dvcnvlem  26034  dvcvx  26079  facth1  26226  elply2  26255  plypf1  26271  coeeq  26286  aaliou3lem8  26405  ulm2  26446  mtestbdd  26466  reeff1o  26509  logbgcd1irr  26855  dcubic2  26905  quart  26922  xrlimcnp  27029  amgm  27052  harmonicbnd4  27072  perfect  27293  dchrptlem1  27326  bposlem2  27347  lgsfcl2  27365  lgsdir  27394  lgsdi  27396  lgsne0  27397  2lgslem1a1  27451  2sqmod  27498  dchrvmasumlem2  27560  chpdifbndlem2  27616  pntpbnd1  27648  pntpbnd2  27649  padicabv  27692  sltres  27725  nolesgn2o  27734  nogesgn1o  27736  nodense  27755  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  noetalem1  27804  nocvxmin  27841  noeta2  27847  readdscl  28449  tgcgrxfr  28544  idmot  28563  legid  28613  btwnleg  28614  leg0  28618  tghilberti1  28663  mirreu3  28680  colperpex  28759  lnopp2hpgb  28789  axcgrrflx  28947  axsegconlem1  28950  axcontlem2  28998  axcontlem12  29008  eengtrkg  29019  wwlksnredwwlkn  29928  0wlkon  30152  0trlon  30156  upgr3v3e3cycl  30212  frgrogt3nreg  30429  nvpi  30699  nmlno0lem  30825  fh1  31650  fh2  31651  nmlnop0iALT  32027  nmopun  32046  branmfn  32137  opsqrlem1  32172  opsqrlem6  32177  mdslmd1lem1  32357  csmdsymi  32366  atom1d  32385  chirredlem2  32423  cdj1i  32465  cdj3i  32473  copsex2dv  32628  fcnvgreu  32691  suppovss  32697  xrofsup  32774  nn0difffzod  32811  pwrssmgc  32973  chnind  32983  gsummpt2d  33032  gsumhashmul  33040  odpmco  33079  cycpmco2lem6  33124  cycpmco2  33126  cyc3evpm  33143  cycpmconjslem2  33148  archirngz  33169  archiabllem2a  33174  rloc0g  33243  rloc1r  33244  sdrgdvcl  33266  sdrginvcl  33267  orngsqr  33299  ornglmullt  33302  orngrmullt  33303  lindssn  33371  lindfpropd  33375  ssdifidllem  33449  ssmxidllem  33466  rsprprmprmidlb  33516  rprmirredb  33525  1arithufd  33541  ply1asclunit  33564  ply1dg1rt  33569  ply1dg3rt0irred  33572  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  lsssra  33603  lindsun  33638  dimkerim  33640  fedgmullem2  33643  irngss  33687  irngnzply1  33691  algextdeglem2  33709  algextdeglem4  33711  metideq  33839  metider  33840  pstmfval  33842  lmxrge0  33898  qqhval2  33928  qqhf  33932  qqhghm  33934  qqhrhm  33935  esumpcvgval  34042  esum2dlem  34056  esum2d  34057  sigainb  34100  insiga  34101  ddemeas  34200  imambfm  34227  dya2icoseg  34242  dya2iocnrect  34246  eulerpartlemgvv  34341  probun  34384  ballotlemfc0  34457  ballotlemfcc  34458  sgnmul  34507  breprexplemc  34609  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  36326  weiunfrlem  36430  weiunso  36432  bj-finsumval0  37251  relowlssretop  37329  wl-2sb6d  37512  tan2h  37572  poimirlem1  37581  poimirlem3  37583  poimirlem4  37584  poimirlem9  37589  poimirlem22  37602  poimirlem28  37608  heicant  37615  mblfinlem2  37618  itg2addnc  37634  ftc2nc  37662  dvasin  37664  sdclem1  37703  fdc  37705  istotbnd3  37731  sstotbnd  37735  prdstotbnd  37754  prdsbnd2  37755  cntotbnd  37756  rngoisocnv  37941  lsmsat  38964  islfld  39018  ps-2  39435  lplnexllnN  39521  4atlem9  39560  4atlem10a  39561  lnatexN  39736  2lnat  39741  pmapjat1  39810  lhpj1  39979  lhpm0atN  39986  4atexlemex2  40028  4atex  40033  4atex2-0aOLDN  40035  4atex2-0cOLDN  40037  lautcnvle  40046  lautj  40050  lautm  40051  idltrn  40107  cdleme01N  40178  cdleme0ex1N  40180  cdleme5  40197  cdleme9  40210  cdleme11c  40218  cdleme11g  40222  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdlemefrs32fva1  40358  cdleme32fva  40394  cdleme32fva1  40395  cdleme32fvaw  40396  cdleme32d  40401  cdleme32f  40403  cdleme35fnpq  40406  cdleme48d  40492  cdleme48gfv  40494  cdleme50ltrn  40514  trlord  40526  cdlemg4b1  40566  cdlemg4b2  40567  cdlemg13a  40608  cdlemg17a  40618  cdlemg17f  40623  erng1lem  40944  erngdvlem3  40947  erngdvlem4  40948  erng1r  40952  erngdvlem3-rN  40955  erngdvlem4-rN  40956  dva0g  40984  dialss  41003  dia0  41009  dia1N  41010  diaglbN  41012  diameetN  41013  diainN  41014  diaintclN  41015  dia1dim  41018  dia2dimlem5  41025  dia2dimlem7  41027  dia2dimlem9  41029  dia2dimlem10  41030  dia2dimlem12  41032  dia2dimlem13  41033  dvhopvadd  41050  dvhvaddass  41054  dvhopvsca  41059  tendolinv  41062  tendorinv  41063  dvhlveclem  41065  dvh0g  41068  dvheveccl  41069  dvhopN  41073  docaclN  41081  diaocN  41082  djajN  41094  dib0  41121  dib1dim  41122  dibglbN  41123  dibintclN  41124  dib1dim2  41125  diblss  41127  diblsmopel  41128  dicvaddcl  41147  dicvscacl  41148  diclspsn  41151  cdlemn4a  41156  cdlemn11c  41166  dihjustlem  41173  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord2cN  41178  dihord11b  41179  dihord11c  41181  dihord2pre  41182  dihlsscpre  41191  dih1dimb  41197  dib2dim  41200  dih2dimb  41201  dih2dimbALTN  41202  dihvalcq2  41204  dihopelvalcpre  41205  dihord6apre  41213  dihord5b  41216  dihord5apre  41219  dih0  41237  dihmeetlem1N  41247  dihglblem5apreN  41248  dihglblem3N  41252  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetlem4preN  41263  dih1dimatlem0  41285  dih1dimatlem  41286  dihatlat  41291  dihatexv  41295  dihglb2  41299  dihmeet  41300  dihintcl  41301  dihmeet2  41303  doch2val2  41321  dochocss  41323  dihoml4c  41333  dochdmj1  41347  djhlj  41358  djhljjN  41359  djhjlj  41360  dihsumssj  41365  djhexmid  41368  djhlsmcl  41371  djhcvat42  41372  dihjatcclem4  41378  dihjat1lem  41385  dihsmsprn  41387  dihjat3  41389  dvh3dim2  41405  dvh3dim3N  41406  dochkr1OLDN  41436  lclkrlem2c  41466  lclkrlem2d  41467  mapdpglem23  41651  hdmap11lem2  41799  0prjspn  42583  mzpcompact2lem  42707  diophrw  42715  rexrabdioph  42750  eldioph4b  42767  pellexlem5  42789  pellfund14  42854  acongtr  42935  fnwe2lem3  43009  gicabl  43056  hbtlem2  43081  hbtlem4  43083  hbtlem5  43085  dgraalem  43102  aaitgo  43119  onexlimgt  43204  onexoegt  43205  oalim2cl  43251  cantnfresb  43286  onmcl  43293  tfsconcatfv  43303  tfsconcatrn  43304  ofoaid1  43320  ofoaid2  43321  ntrclsk13  44033  gneispb  44093  wessf1ornlem  45092  ltdiv23neg  45309  islptre  45540  limclner  45572  icccncfext  45808  stoweidlem1  45922  stoweidlem14  45935  stoweidlem24  45945  stoweidlem46  45967  stoweidlem57  45978  dirkercncflem2  46025  fourierdlem20  46048  fourierdlem41  46069  fourierdlem46  46073  fourierdlem48  46075  fourierdlem50  46077  fourierdlem62  46089  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem76  46103  fourierdlem79  46106  fourierdlem103  46130  fourierdlem104  46131  etransclem47  46202  iccpartiun  47308  reupr  47396  sqrtpwpw2p  47412  fmtnoprmfac1lem  47438  fmtnoprmfac2lem1  47440  lighneallem4a  47482  requad2  47497  perfectALTV  47597  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  isuspgrim0lem  47755  isuspgrim0  47756  isuspgrimlem  47758  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrimlem  47785  grimgrtri  47798  gsumlsscl  48108  lincsumcl  48160  lincscmcl  48161  isldepslvec2  48214  m1modmmod  48255  elbigo2  48286  relogbdivb  48296  blennnt2  48323  dignn0ldlem  48336  itsclc0yqsollem2  48497  inlinecirc02p  48521  lubeldm2  48636  glbeldm2  48637  lubsscl  48640  glbsscl  48641  isclatd  48655  fullthinc  48713