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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  syl22anc  838  raaan  4521  raaanv  4522  raaan2  4525  soltmin  6138  xpdifid  6168  reuop  6293  f1dom3fv3dif  7267  f1prex  7282  cocan1  7289  fliftfun  7309  soisores  7324  soisoi  7325  isopolem  7342  f1oiso2  7349  weniso  7351  caovcld  7600  caovcomd  7603  onminex  7790  poxp2  8129  poxp3  8136  poseq  8144  tfrlem12  8389  omeulem1  8582  oaabs2  8648  omabs  8650  eldifsucnn  8663  naddcllem  8675  erov  8808  findcard2d  9166  frfi  9288  finsschain  9359  suplub2  9456  supgtoreq  9465  supisolem  9468  ordiso2  9510  ordtypelem7  9519  wemaplem2  9542  wemapsolem  9545  cantnflt  9667  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1  9684  wemapwe  9692  cnfcomlem  9694  cnfcom  9695  cnfcom3lem  9698  infxpenlem  10008  fseqenlem1  10019  dfac12lem2  10139  infpssrlem4  10301  enfin2i  10316  isf34lem7  10374  isf34lem6  10375  fin1a2lem7  10401  fin1a2lem10  10404  fin1a2lem11  10405  fin1a2lem13  10407  ttukeylem6  10509  ttukeylem7  10510  iundom2g  10535  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  fpwwe2lem11  10636  fpwwe2  10638  canthnumlem  10643  canthwelem  10645  canthp1lem2  10648  pwfseqlem4  10657  inar1  10770  intgru  10809  distrlem4pr  11021  conjmul  11931  lediv12a  12107  recp1lt1  12112  cju  12208  gtndiv  12639  zsupss  12921  uzsupss  12924  icc0  13372  iccssioo2  13397  fzrev3  13567  ico01fl0  13784  fldiv  13825  modabs  13869  modltm1p1mod  13888  modifeq2int  13898  modsumfzodifsn  13909  seqcaopr  14005  seqf1olem1  14007  seqof2  14026  crreczi  14191  seqcoll  14425  seqcoll2  14426  hashtpg  14446  swrdccat3b  14690  01sqrexlem2  15190  resqrex  15197  abs1m  15282  isercoll  15614  zsum  15664  fsum2dlem  15716  fsumcom2  15720  fprod2dlem  15924  fprodcom2  15928  efsub  16043  bitsinv2  16384  sqgcd  16502  qredeu  16595  isprm7  16645  pcpremul  16776  pceulem  16778  pczpre  16780  pcdiv  16785  pcqmul  16786  pcqdiv  16790  pcexp  16792  pcdvdsb  16802  pcneg  16807  pcdvdstr  16809  pcgcd1  16810  pc2dvds  16812  pcz  16814  pcaddlem  16821  pcadd  16822  qexpz  16834  expnprm  16835  infpnlem2  16844  ramub2  16947  ramub1lem1  16959  setsstruct2  17107  f1ocpbllem  17470  f1ovscpbl  17472  mreexexlem3d  17590  mreexexlem4d  17591  fthi  17869  ipodrsima  18494  sgrppropd  18622  mndpropd  18650  grpsubpropd2  18929  ghmf1  19121  symgfvne  19248  f1omvdmvd  19311  f1otrspeq  19315  pmtrdifwrdel  19353  pmtrdifwrdel2  19354  psgnunilem2  19363  psgnunilem3  19364  psgnvalii  19377  odf1  19430  lsmpropd  19545  ablnnncan  19690  gsummptshft  19804  dprdf1o  19902  pgpfac1lem3  19947  pgpfac1lem5  19949  pgpfaclem1  19951  ablfaclem2  19956  srgbinomlem3  20051  ringpropd  20102  f1ghm0to0  20279  lmodprop2d  20534  lsspropd  20628  lmhmpropd  20684  lbspropd  20710  lbsextlem3  20773  iporthcom  21188  obslbs  21285  assapropd  21426  psrass1  21525  psrass23l  21528  psrass23  21530  mplsubrg  21564  mplmon  21590  mplmonmul  21591  mplcoe1  21592  mplbas2  21597  mplind  21631  evlslem2  21642  mpfind  21670  gsumply1subr  21756  psrplusgpropd  21758  ply1scln0  21814  scmataddcl  22018  scmatsubcl  22019  scmatmulcl  22020  smatvscl  22026  scmatrhmcl  22030  mat1scmat  22041  smadiadetglem2  22174  cramerimplem2  22186  cramerimplem3  22187  cramerimp  22188  1pmatscmul  22204  mat2pmatf1  22231  pm2mp  22327  chmatcl  22330  chmatval  22331  chmaidscmat  22350  chfacfisf  22356  cayhamlem1  22368  cpmidgsumm2pm  22371  cpmidpmat  22375  cpmadugsumfi  22379  cpmadumatpoly  22385  cayhamlem3  22389  pptbas  22511  elcls  22577  neiint  22608  neiptopnei  22636  restbas  22662  neitr  22684  iscnp4  22767  cnconst2  22787  cnpdis  22797  cnt0  22850  cnhaus  22858  cmpcovf  22895  hauscmplem  22910  conncompid  22935  2ndci  22952  2ndc1stc  22955  1stcrest  22957  2ndcctbss  22959  2ndcomap  22962  2ndcsep  22963  dis2ndc  22964  restlly  22987  islly2  22988  lly1stc  23000  dislly  23001  finlocfin  23024  dissnlocfin  23033  locfindis  23034  llycmpkgen2  23054  ptbasfi  23085  neitx  23111  ptpjopn  23116  ptcnplem  23125  upxp  23127  txlly  23140  txtube  23144  tx1stc  23154  txkgen  23156  xkococnlem  23163  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  hmeoimaf1o  23274  reghmph  23297  nrmhmph  23298  ordthmeolem  23305  trfil2  23391  fmfnfm  23462  hauspwpwf1  23491  fclsfnflim  23531  cnextf  23570  cnextcn  23571  tmdgsum2  23600  symgtgp  23610  subgntr  23611  opnsubg  23612  ghmcnp  23619  qustgpopn  23624  tsmsf1o  23649  tsmsxplem1  23657  tsmsxplem2  23658  tsmsxp  23659  ustexsym  23720  restutop  23742  imasdsf1olem  23879  blssexps  23932  blssex  23933  ssblex  23934  imasf1oxms  23998  blcld  24014  stdbdmopn  24027  met1stc  24030  met2ndci  24031  prdsxmslem2  24038  metcnp3  24049  cfilucfil  24068  ngptgp  24145  tgioo  24312  tgqioo  24316  zdis  24332  iccpnfhmeo  24461  xrhmeo  24462  cnheibor  24471  elpi1i  24562  cmetcusp  24871  bncssbn  24891  pjthlem2  24955  ivthlem2  24969  ovolicc1  25033  ovolicc2lem3  25036  ovolicc2lem4  25037  volsup  25073  volivth  25124  vitalilem3  25127  mbflimsup  25183  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem5  25237  limcnlp  25395  limcflf  25398  limciun  25411  dvmptfsum  25492  dvcnvlem  25493  dvcvx  25537  facth1  25682  elply2  25710  plypf1  25726  coeeq  25741  aaliou3lem8  25858  ulm2  25897  mtestbdd  25917  reeff1o  25959  logbgcd1irr  26299  dcubic2  26349  quart  26366  xrlimcnp  26473  amgm  26495  harmonicbnd4  26515  perfect  26734  dchrptlem1  26767  bposlem2  26788  lgsfcl2  26806  lgsdir  26835  lgsdi  26837  lgsne0  26838  2lgslem1a1  26892  2sqmod  26939  dchrvmasumlem2  27001  chpdifbndlem2  27057  pntpbnd1  27089  pntpbnd2  27090  padicabv  27133  sltres  27165  nolesgn2o  27174  nogesgn1o  27176  nodense  27195  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfres  27225  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  noetalem1  27244  nocvxmin  27280  noeta2  27286  tgcgrxfr  27769  idmot  27788  legid  27838  btwnleg  27839  leg0  27843  tghilberti1  27888  mirreu3  27905  colperpex  27984  lnopp2hpgb  28014  axcgrrflx  28172  axsegconlem1  28175  axcontlem2  28223  axcontlem12  28233  eengtrkg  28244  wwlksnredwwlkn  29149  0wlkon  29373  0trlon  29377  upgr3v3e3cycl  29433  frgrogt3nreg  29650  nvpi  29920  nmlno0lem  30046  fh1  30871  fh2  30872  nmlnop0iALT  31248  nmopun  31267  branmfn  31358  opsqrlem1  31393  opsqrlem6  31398  mdslmd1lem1  31578  csmdsymi  31587  atom1d  31606  chirredlem2  31644  cdj1i  31686  cdj3i  31694  fcnvgreu  31898  suppovss  31906  xrofsup  31980  nn0difffzod  32016  pwrssmgc  32170  gsummpt2d  32201  gsumhashmul  32208  odpmco  32247  cycpmco2lem6  32290  cycpmco2  32292  cyc3evpm  32309  cycpmconjslem2  32314  archirngz  32335  archiabllem2a  32340  sdrgdvcl  32397  sdrginvcl  32398  orngsqr  32422  ornglmullt  32425  orngrmullt  32426  lindssn  32494  lindfpropd  32498  ghmqusker  32532  ssmxidllem  32589  evls1addd  32648  evls1muld  32649  evls1vsca  32650  ply1asclunit  32654  asclply1subcl  32660  ply1degltel  32666  ply1degltlss  32667  lindsun  32710  dimkerim  32712  fedgmullem2  32715  irngss  32751  irngnzply1  32755  algextdeglem1  32772  metideq  32873  metider  32874  pstmfval  32876  lmxrge0  32932  qqhval2  32962  qqhf  32966  qqhghm  32968  qqhrhm  32969  esumpcvgval  33076  esum2dlem  33090  esum2d  33091  sigainb  33134  insiga  33135  ddemeas  33234  imambfm  33261  dya2icoseg  33276  dya2iocnrect  33280  eulerpartlemgvv  33375  probun  33418  ballotlemfc0  33491  ballotlemfcc  33492  sgnmul  33541  breprexplemc  33644  erdszelem8  34189  erdszelem9  34190  erdsze2lem2  34195  cnpconn  34221  txpconn  34223  ptpconn  34224  indispconn  34225  connpconn  34226  cvxpconn  34233  cnllysconn  34236  cvmcov2  34266  cvmopnlem  34269  cvmliftmolem1  34272  cvmliftlem14  34288  cvmliftlem15  34289  cvmlift2lem13  34306  cvmlift3lem2  34311  cvmlift3lem9  34318  seglerflx  35084  seglemin  35085  btwnsegle  35089  hilbert1.1  35126  neibastop2lem  35245  bj-finsumval0  36166  relowlssretop  36244  wl-2sb6d  36423  tan2h  36480  poimirlem1  36489  poimirlem3  36491  poimirlem4  36492  poimirlem9  36497  poimirlem22  36510  poimirlem28  36516  heicant  36523  mblfinlem2  36526  itg2addnc  36542  ftc2nc  36570  dvasin  36572  sdclem1  36611  fdc  36613  istotbnd3  36639  sstotbnd  36643  prdstotbnd  36662  prdsbnd2  36663  cntotbnd  36664  rngoisocnv  36849  lsmsat  37878  islfld  37932  ps-2  38349  lplnexllnN  38435  4atlem9  38474  4atlem10a  38475  lnatexN  38650  2lnat  38655  pmapjat1  38724  lhpj1  38893  lhpm0atN  38900  4atexlemex2  38942  4atex  38947  4atex2-0aOLDN  38949  4atex2-0cOLDN  38951  lautcnvle  38960  lautj  38964  lautm  38965  idltrn  39021  cdleme01N  39092  cdleme0ex1N  39094  cdleme5  39111  cdleme9  39124  cdleme11c  39132  cdleme11g  39136  cdlemefrs29bpre0  39267  cdlemefrs29cpre1  39269  cdlemefrs32fva1  39272  cdleme32fva  39308  cdleme32fva1  39309  cdleme32fvaw  39310  cdleme32d  39315  cdleme32f  39317  cdleme35fnpq  39320  cdleme48d  39406  cdleme48gfv  39408  cdleme50ltrn  39428  trlord  39440  cdlemg4b1  39480  cdlemg4b2  39481  cdlemg13a  39522  cdlemg17a  39532  cdlemg17f  39537  erng1lem  39858  erngdvlem3  39861  erngdvlem4  39862  erng1r  39866  erngdvlem3-rN  39869  erngdvlem4-rN  39870  dva0g  39898  dialss  39917  dia0  39923  dia1N  39924  diaglbN  39926  diameetN  39927  diainN  39928  diaintclN  39929  dia1dim  39932  dia2dimlem5  39939  dia2dimlem7  39941  dia2dimlem9  39943  dia2dimlem10  39944  dia2dimlem12  39946  dia2dimlem13  39947  dvhopvadd  39964  dvhvaddass  39968  dvhopvsca  39973  tendolinv  39976  tendorinv  39977  dvhlveclem  39979  dvh0g  39982  dvheveccl  39983  dvhopN  39987  docaclN  39995  diaocN  39996  djajN  40008  dib0  40035  dib1dim  40036  dibglbN  40037  dibintclN  40038  dib1dim2  40039  diblss  40041  diblsmopel  40042  dicvaddcl  40061  dicvscacl  40062  diclspsn  40065  cdlemn4a  40070  cdlemn11c  40080  dihjustlem  40087  dihord1  40089  dihord2a  40090  dihord2b  40091  dihord2cN  40092  dihord11b  40093  dihord11c  40095  dihord2pre  40096  dihlsscpre  40105  dih1dimb  40111  dib2dim  40114  dih2dimb  40115  dih2dimbALTN  40116  dihvalcq2  40118  dihopelvalcpre  40119  dihord6apre  40127  dihord5b  40130  dihord5apre  40133  dih0  40151  dihmeetlem1N  40161  dihglblem5apreN  40162  dihglblem3N  40166  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetlem4preN  40177  dih1dimatlem0  40199  dih1dimatlem  40200  dihatlat  40205  dihatexv  40209  dihglb2  40213  dihmeet  40214  dihintcl  40215  dihmeet2  40217  doch2val2  40235  dochocss  40237  dihoml4c  40247  dochdmj1  40261  djhlj  40272  djhljjN  40273  djhjlj  40274  dihsumssj  40279  djhexmid  40282  djhlsmcl  40285  djhcvat42  40286  dihjatcclem4  40292  dihjat1lem  40299  dihsmsprn  40301  dihjat3  40303  dvh3dim2  40319  dvh3dim3N  40320  dochkr1OLDN  40350  lclkrlem2c  40380  lclkrlem2d  40381  mapdpglem23  40565  hdmap11lem2  40713  expgcd  41225  0prjspn  41370  mzpcompact2lem  41489  diophrw  41497  rexrabdioph  41532  eldioph4b  41549  pellexlem5  41571  pellfund14  41636  acongtr  41717  fnwe2lem3  41794  gicabl  41841  hbtlem2  41866  hbtlem4  41868  hbtlem5  41870  dgraalem  41887  aaitgo  41904  onexlimgt  41992  onexoegt  41993  oalim2cl  42039  cantnfresb  42074  onmcl  42081  tfsconcatfv  42091  tfsconcatrn  42092  ofoaid1  42108  ofoaid2  42109  ntrclsk13  42822  gneispb  42882  wessf1ornlem  43882  ltdiv23neg  44104  islptre  44335  limclner  44367  icccncfext  44603  stoweidlem1  44717  stoweidlem14  44730  stoweidlem24  44740  stoweidlem46  44762  stoweidlem57  44773  dirkercncflem2  44820  fourierdlem20  44843  fourierdlem41  44864  fourierdlem46  44868  fourierdlem48  44870  fourierdlem50  44872  fourierdlem62  44884  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem76  44898  fourierdlem79  44901  fourierdlem103  44925  fourierdlem104  44926  etransclem47  44997  iccpartiun  46102  reupr  46190  sqrtpwpw2p  46206  fmtnoprmfac1lem  46232  fmtnoprmfac2lem1  46234  lighneallem4a  46276  requad2  46291  perfectALTV  46391  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  mgmpropd  46545  rngpropd  46673  gsumlsscl  47059  lincsumcl  47112  lincscmcl  47113  isldepslvec2  47166  m1modmmod  47207  elbigo2  47238  relogbdivb  47248  blennnt2  47275  dignn0ldlem  47288  itsclc0yqsollem2  47449  inlinecirc02p  47473  lubeldm2  47589  glbeldm2  47590  lubsscl  47593  glbsscl  47594  isclatd  47608  fullthinc  47666