Theorem syl12anc 837

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl22anc  839  raaan  4432  raaanv  4433  raaan2  4436  soltmin  6001  xpdifid  6031  reuop  6156  f1dom3fv3dif  7080  f1prex  7094  cocan1  7101  fliftfun  7121  soisores  7136  soisoi  7137  isopolem  7154  f1oiso2  7161  weniso  7163  caovcld  7401  caovcomd  7404  onminex  7586  tfrlem12  8125  omeulem1  8310  oaabs2  8374  omabs  8376  erov  8496  findcard2d  8844  frfi  8916  finsschain  8983  suplub2  9077  supgtoreq  9086  supisolem  9089  ordiso2  9131  ordtypelem7  9140  wemaplem2  9163  wemapsolem  9166  cantnflt  9287  cantnfp1lem3  9295  cantnflem1b  9301  cantnflem1  9304  wemapwe  9312  cnfcomlem  9314  cnfcom  9315  cnfcom3lem  9318  infxpenlem  9627  fseqenlem1  9638  dfac12lem2  9758  infpssrlem4  9920  enfin2i  9935  isf34lem7  9993  isf34lem6  9994  fin1a2lem7  10020  fin1a2lem10  10023  fin1a2lem11  10024  fin1a2lem13  10026  ttukeylem6  10128  ttukeylem7  10129  iundom2g  10154  fpwwe2lem5  10249  fpwwe2lem6  10250  fpwwe2lem8  10252  fpwwe2lem11  10255  fpwwe2  10257  canthnumlem  10262  canthwelem  10264  canthp1lem2  10267  pwfseqlem4  10276  inar1  10389  intgru  10428  distrlem4pr  10640  conjmul  11549  lediv12a  11725  recp1lt1  11730  cju  11826  gtndiv  12254  zsupss  12533  uzsupss  12536  icc0  12983  iccssioo2  13008  fzrev3  13178  ico01fl0  13394  fldiv  13433  modabs  13477  modltm1p1mod  13496  modifeq2int  13506  modsumfzodifsn  13517  seqcaopr  13613  seqf1olem1  13615  seqof2  13634  crreczi  13795  seqcoll  14030  seqcoll2  14031  hashtpg  14051  swrdccat3b  14305  sqrlem2  14807  resqrex  14814  abs1m  14899  isercoll  15231  zsum  15282  fsum2dlem  15334  fsumcom2  15338  fprod2dlem  15542  fprodcom2  15546  efsub  15661  bitsinv2  16002  sqgcd  16122  qredeu  16215  isprm7  16265  pcpremul  16396  pceulem  16398  pczpre  16400  pcdiv  16405  pcqmul  16406  pcqdiv  16410  pcexp  16412  pcdvdsb  16422  pcneg  16427  pcdvdstr  16429  pcgcd1  16430  pc2dvds  16432  pcz  16434  pcaddlem  16441  pcadd  16442  qexpz  16454  expnprm  16455  infpnlem2  16464  ramub2  16567  ramub1lem1  16579  setsstruct2  16727  f1ocpbllem  17029  f1ovscpbl  17031  mreexexlem3d  17149  mreexexlem4d  17150  fthi  17425  ipodrsima  18047  mndpropd  18198  grpsubpropd2  18469  ghmf1  18651  symgfvne  18773  f1omvdmvd  18835  f1otrspeq  18839  pmtrdifwrdel  18877  pmtrdifwrdel2  18878  psgnunilem2  18887  psgnunilem3  18888  psgnvalii  18901  odf1  18953  lsmpropd  19067  ablnnncan  19208  gsummptshft  19321  dprdf1o  19419  pgpfac1lem3  19464  pgpfac1lem5  19466  pgpfaclem1  19468  ablfaclem2  19473  srgbinomlem3  19557  ringpropd  19600  f1ghm0to0  19760  lmodprop2d  19961  lsspropd  20054  lmhmpropd  20110  lbspropd  20136  lbsextlem3  20197  iporthcom  20597  obslbs  20692  assapropd  20831  psrass1  20930  psrass23l  20933  psrass23  20935  mplsubrg  20967  mplmon  20992  mplmonmul  20993  mplcoe1  20994  mplbas2  20999  mplind  21028  evlslem2  21039  mpfind  21067  gsumply1subr  21155  psrplusgpropd  21157  ply1scln0  21212  scmataddcl  21413  scmatsubcl  21414  scmatmulcl  21415  smatvscl  21421  scmatrhmcl  21425  mat1scmat  21436  smadiadetglem2  21569  cramerimplem2  21581  cramerimplem3  21582  cramerimp  21583  1pmatscmul  21599  mat2pmatf1  21626  pm2mp  21722  chmatcl  21725  chmatval  21726  chmaidscmat  21745  chfacfisf  21751  cayhamlem1  21763  cpmidgsumm2pm  21766  cpmidpmat  21770  cpmadugsumfi  21774  cpmadumatpoly  21780  cayhamlem3  21784  pptbas  21905  elcls  21970  neiint  22001  neiptopnei  22029  restbas  22055  neitr  22077  iscnp4  22160  cnconst2  22180  cnpdis  22190  cnt0  22243  cnhaus  22251  cmpcovf  22288  hauscmplem  22303  conncompid  22328  2ndci  22345  2ndc1stc  22348  1stcrest  22350  2ndcctbss  22352  2ndcomap  22355  2ndcsep  22356  dis2ndc  22357  restlly  22380  islly2  22381  lly1stc  22393  dislly  22394  finlocfin  22417  dissnlocfin  22426  locfindis  22427  llycmpkgen2  22447  ptbasfi  22478  neitx  22504  ptpjopn  22509  ptcnplem  22518  upxp  22520  txlly  22533  txtube  22537  tx1stc  22547  txkgen  22549  xkococnlem  22556  kqreglem1  22638  kqreglem2  22639  kqnrmlem1  22640  kqnrmlem2  22641  hmeoimaf1o  22667  reghmph  22690  nrmhmph  22691  ordthmeolem  22698  trfil2  22784  fmfnfm  22855  hauspwpwf1  22884  fclsfnflim  22924  cnextf  22963  cnextcn  22964  tmdgsum2  22993  symgtgp  23003  subgntr  23004  opnsubg  23005  ghmcnp  23012  qustgpopn  23017  tsmsf1o  23042  tsmsxplem1  23050  tsmsxplem2  23051  tsmsxp  23052  ustexsym  23113  restutop  23135  imasdsf1olem  23271  blssexps  23324  blssex  23325  ssblex  23326  imasf1oxms  23387  blcld  23403  stdbdmopn  23416  met1stc  23419  met2ndci  23420  prdsxmslem2  23427  metcnp3  23438  cfilucfil  23457  ngptgp  23534  tgioo  23693  tgqioo  23697  zdis  23713  iccpnfhmeo  23842  xrhmeo  23843  cnheibor  23852  elpi1i  23943  cmetcusp  24251  bncssbn  24271  pjthlem2  24335  ivthlem2  24349  ovolicc1  24413  ovolicc2lem3  24416  ovolicc2lem4  24417  volsup  24453  volivth  24504  vitalilem3  24507  mbflimsup  24563  mbfi1fseqlem1  24613  mbfi1fseqlem3  24615  mbfi1fseqlem5  24617  limcnlp  24775  limcflf  24778  limciun  24791  dvmptfsum  24872  dvcnvlem  24873  dvcvx  24917  facth1  25062  elply2  25090  plypf1  25106  coeeq  25121  aaliou3lem8  25238  ulm2  25277  mtestbdd  25297  reeff1o  25339  logbgcd1irr  25677  dcubic2  25727  quart  25744  xrlimcnp  25851  amgm  25873  harmonicbnd4  25893  perfect  26112  dchrptlem1  26145  bposlem2  26166  lgsfcl2  26184  lgsdir  26213  lgsdi  26215  lgsne0  26216  2lgslem1a1  26270  2sqmod  26317  dchrvmasumlem2  26379  chpdifbndlem2  26435  pntpbnd1  26467  pntpbnd2  26468  padicabv  26511  tgcgrxfr  26609  idmot  26628  legid  26678  btwnleg  26679  leg0  26683  tghilberti1  26728  mirreu3  26745  colperpex  26824  lnopp2hpgb  26854  axcgrrflx  27005  axsegconlem1  27008  axcontlem2  27056  axcontlem12  27066  eengtrkg  27077  wwlksnredwwlkn  27979  0wlkon  28203  0trlon  28207  upgr3v3e3cycl  28263  frgrogt3nreg  28480  nvpi  28748  nmlno0lem  28874  fh1  29699  fh2  29700  nmlnop0iALT  30076  nmopun  30095  branmfn  30186  opsqrlem1  30221  opsqrlem6  30226  mdslmd1lem1  30406  csmdsymi  30415  atom1d  30434  chirredlem2  30472  cdj1i  30514  cdj3i  30522  fcnvgreu  30730  suppovss  30737  xrofsup  30810  pwrssmgc  30997  gsummpt2d  31028  gsumhashmul  31035  odpmco  31074  cycpmco2lem6  31117  cycpmco2  31119  cyc3evpm  31136  cycpmconjslem2  31141  archirngz  31162  archiabllem2a  31167  orngsqr  31222  ornglmullt  31225  orngrmullt  31226  lindssn  31287  lindfpropd  31290  ssmxidllem  31355  lindsun  31420  dimkerim  31422  fedgmullem2  31425  metideq  31557  metider  31558  pstmfval  31560  lmxrge0  31616  qqhval2  31644  qqhf  31648  qqhghm  31650  qqhrhm  31651  esumpcvgval  31758  esum2dlem  31772  esum2d  31773  sigainb  31816  insiga  31817  ddemeas  31916  imambfm  31941  dya2icoseg  31956  dya2iocnrect  31960  eulerpartlemgvv  32055  probun  32098  ballotlemfc0  32171  ballotlemfcc  32172  sgnmul  32221  breprexplemc  32324  erdszelem8  32873  erdszelem9  32874  erdsze2lem2  32879  cnpconn  32905  txpconn  32907  ptpconn  32908  indispconn  32909  connpconn  32910  cvxpconn  32917  cnllysconn  32920  cvmcov2  32950  cvmopnlem  32953  cvmliftmolem1  32956  cvmliftlem14  32972  cvmliftlem15  32973  cvmlift2lem13  32990  cvmlift3lem2  32995  cvmlift3lem9  33002  eldifsucnn  33410  poxp2  33527  poxp3  33533  poseq  33539  naddcllem  33568  sltres  33602  nolesgn2o  33611  nogesgn1o  33613  nodense  33632  nosupbnd1lem3  33650  nosupbnd1lem5  33652  nosupbnd2lem1  33655  noinfres  33662  noinfbnd1lem3  33665  noinfbnd1lem5  33667  noinfbnd2lem1  33670  noetalem1  33681  nocvxmin  33710  noeta2  33716  seglerflx  34151  seglemin  34152  btwnsegle  34156  hilbert1.1  34193  neibastop2lem  34286  bj-finsumval0  35191  relowlssretop  35271  wl-2sb6d  35450  tan2h  35506  poimirlem1  35515  poimirlem3  35517  poimirlem4  35518  poimirlem9  35523  poimirlem22  35536  poimirlem28  35542  heicant  35549  mblfinlem2  35552  itg2addnc  35568  ftc2nc  35596  dvasin  35598  sdclem1  35638  fdc  35640  istotbnd3  35666  sstotbnd  35670  prdstotbnd  35689  prdsbnd2  35690  cntotbnd  35691  rngoisocnv  35876  lsmsat  36759  islfld  36813  ps-2  37229  lplnexllnN  37315  4atlem9  37354  4atlem10a  37355  lnatexN  37530  2lnat  37535  pmapjat1  37604  lhpj1  37773  lhpm0atN  37780  4atexlemex2  37822  4atex  37827  4atex2-0aOLDN  37829  4atex2-0cOLDN  37831  lautcnvle  37840  lautj  37844  lautm  37845  idltrn  37901  cdleme01N  37972  cdleme0ex1N  37974  cdleme5  37991  cdleme9  38004  cdleme11c  38012  cdleme11g  38016  cdlemefrs29bpre0  38147  cdlemefrs29cpre1  38149  cdlemefrs32fva1  38152  cdleme32fva  38188  cdleme32fva1  38189  cdleme32fvaw  38190  cdleme32d  38195  cdleme32f  38197  cdleme35fnpq  38200  cdleme48d  38286  cdleme48gfv  38288  cdleme50ltrn  38308  trlord  38320  cdlemg4b1  38360  cdlemg4b2  38361  cdlemg13a  38402  cdlemg17a  38412  cdlemg17f  38417  erng1lem  38738  erngdvlem3  38741  erngdvlem4  38742  erng1r  38746  erngdvlem3-rN  38749  erngdvlem4-rN  38750  dva0g  38778  dialss  38797  dia0  38803  dia1N  38804  diaglbN  38806  diameetN  38807  diainN  38808  diaintclN  38809  dia1dim  38812  dia2dimlem5  38819  dia2dimlem7  38821  dia2dimlem9  38823  dia2dimlem10  38824  dia2dimlem12  38826  dia2dimlem13  38827  dvhopvadd  38844  dvhvaddass  38848  dvhopvsca  38853  tendolinv  38856  tendorinv  38857  dvhlveclem  38859  dvh0g  38862  dvheveccl  38863  dvhopN  38867  docaclN  38875  diaocN  38876  djajN  38888  dib0  38915  dib1dim  38916  dibglbN  38917  dibintclN  38918  dib1dim2  38919  diblss  38921  diblsmopel  38922  dicvaddcl  38941  dicvscacl  38942  diclspsn  38945  cdlemn4a  38950  cdlemn11c  38960  dihjustlem  38967  dihord1  38969  dihord2a  38970  dihord2b  38971  dihord2cN  38972  dihord11b  38973  dihord11c  38975  dihord2pre  38976  dihlsscpre  38985  dih1dimb  38991  dib2dim  38994  dih2dimb  38995  dih2dimbALTN  38996  dihvalcq2  38998  dihopelvalcpre  38999  dihord6apre  39007  dihord5b  39010  dihord5apre  39013  dih0  39031  dihmeetlem1N  39041  dihglblem5apreN  39042  dihglblem3N  39046  dihmeetlem2N  39050  dihglbcpreN  39051  dihmeetlem4preN  39057  dih1dimatlem0  39079  dih1dimatlem  39080  dihatlat  39085  dihatexv  39089  dihglb2  39093  dihmeet  39094  dihintcl  39095  dihmeet2  39097  doch2val2  39115  dochocss  39117  dihoml4c  39127  dochdmj1  39141  djhlj  39152  djhljjN  39153  djhjlj  39154  dihsumssj  39159  djhexmid  39162  djhlsmcl  39165  djhcvat42  39166  dihjatcclem4  39172  dihjat1lem  39179  dihsmsprn  39181  dihjat3  39183  dvh3dim2  39199  dvh3dim3N  39200  dochkr1OLDN  39230  lclkrlem2c  39260  lclkrlem2d  39261  mapdpglem23  39445  hdmap11lem2  39593  expgcd  40042  0prjspn  40173  mzpcompact2lem  40276  diophrw  40284  rexrabdioph  40319  eldioph4b  40336  pellexlem5  40358  pellfund14  40423  acongtr  40503  fnwe2lem3  40580  gicabl  40627  hbtlem2  40652  hbtlem4  40654  hbtlem5  40656  dgraalem  40673  aaitgo  40690  ntrclsk13  41358  gneispb  41418  wessf1ornlem  42395  ltdiv23neg  42607  islptre  42835  limclner  42867  icccncfext  43103  stoweidlem1  43217  stoweidlem14  43230  stoweidlem24  43240  stoweidlem46  43262  stoweidlem57  43273  dirkercncflem2  43320  fourierdlem20  43343  fourierdlem41  43364  fourierdlem46  43368  fourierdlem48  43370  fourierdlem50  43372  fourierdlem62  43384  fourierdlem63  43385  fourierdlem64  43386  fourierdlem65  43387  fourierdlem76  43398  fourierdlem79  43401  fourierdlem103  43425  fourierdlem104  43426  etransclem47  43497  iccpartiun  44559  reupr  44647  sqrtpwpw2p  44663  fmtnoprmfac1lem  44689  fmtnoprmfac2lem1  44691  lighneallem4a  44733  requad2  44748  perfectALTV  44848  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  mgmpropd  45002  lidlmmgm  45156  gsumlsscl  45392  lincsumcl  45445  lincscmcl  45446  isldepslvec2  45499  m1modmmod  45540  elbigo2  45571  relogbdivb  45581  blennnt2  45608  dignn0ldlem  45621  itsclc0yqsollem2  45782  inlinecirc02p  45806  lubeldm2  45923  glbeldm2  45924  lubsscl  45927  glbsscl  45928  isclatd  45942  fullthinc  46000