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  4480  raaanv  4481  raaan2  4484  copsex2dv  5454  soltmin  6109  xpdifid  6141  reuop  6266  f1dom3fv3dif  7243  f1prex  7259  cocan1  7266  fliftfun  7287  soisores  7302  soisoi  7303  isopolem  7320  f1oiso2  7327  weniso  7329  caovcld  7582  caovcomd  7585  onminex  7778  poxp2  8122  poxp3  8129  poseq  8137  tfrlem12  8357  omeulem1  8546  nnaordex2  8603  oaabs2  8613  omabs  8615  eldifsucnn  8628  naddcllem  8640  erov  8787  findcard2d  9130  frfi  9232  finsschain  9310  suplub2  9412  supgtoreq  9422  supisolem  9425  ordiso2  9468  ordtypelem7  9477  wemaplem2  9500  wemapsolem  9503  cantnflt  9625  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  wemapwe  9650  cnfcomlem  9652  cnfcom  9653  cnfcom3lem  9656  infxpenlem  9966  fseqenlem1  9977  dfac12lem2  10098  infpssrlem4  10259  enfin2i  10274  isf34lem7  10332  isf34lem6  10333  fin1a2lem7  10359  fin1a2lem10  10362  fin1a2lem11  10363  fin1a2lem13  10365  ttukeylem6  10467  ttukeylem7  10468  iundom2g  10493  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem11  10594  fpwwe2  10596  canthnumlem  10601  canthwelem  10603  canthp1lem2  10606  pwfseqlem4  10615  inar1  10728  intgru  10767  distrlem4pr  10979  conjmul  11899  lediv12a  12076  recp1lt1  12081  cju  12182  gtndiv  12611  zsupss  12896  uzsupss  12899  icc0  13354  iccssioo2  13380  fzrev3  13551  ico01fl0  13781  fldiv  13822  modabs  13866  modltm1p1mod  13888  modifeq2int  13898  modsumfzodifsn  13909  seqcaopr  14004  seqf1olem1  14006  seqof2  14025  crreczi  14193  seqcoll  14429  seqcoll2  14430  hashtpg  14450  swrdccat3b  14705  01sqrexlem2  15209  resqrex  15216  abs1m  15302  isercoll  15634  zsum  15684  fsum2dlem  15736  fsumcom2  15740  fprod2dlem  15946  fprodcom2  15950  efsub  16068  bitsinv2  16413  sqgcd  16532  expgcd  16533  qredeu  16628  isprm7  16678  pcpremul  16814  pceulem  16816  pczpre  16818  pcdiv  16823  pcqmul  16824  pcqdiv  16828  pcexp  16830  pcdvdsb  16840  pcneg  16845  pcdvdstr  16847  pcgcd1  16848  pc2dvds  16850  pcz  16852  pcaddlem  16859  pcadd  16860  qexpz  16872  expnprm  16873  infpnlem2  16882  ramub2  16985  ramub1lem1  16997  setsstruct2  17144  f1ocpbllem  17487  f1ovscpbl  17489  mreexexlem3d  17607  mreexexlem4d  17608  fthi  17882  ipodrsima  18500  mgmpropd  18578  sgrppropd  18658  mndpropd  18686  grpsubpropd2  18978  f1ghm0to0  19177  ghmqusker  19219  symgfvne  19311  f1omvdmvd  19373  f1otrspeq  19377  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  psgnunilem2  19425  psgnunilem3  19426  psgnvalii  19439  odf1  19492  lsmpropd  19607  ablnnncan  19752  gsummptshft  19866  dprdf1o  19964  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfaclem1  20013  ablfaclem2  20018  rngpropd  20083  srgbinomlem3  20137  ringpropd  20197  lmodprop2d  20830  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  lbsextlem3  21070  iporthcom  21544  obslbs  21639  assapropd  21781  psrass1  21873  psrass23l  21876  psrass23  21878  mplsubrg  21914  mplmon  21942  mplmonmul  21943  mplcoe1  21944  mplbas2  21949  mplind  21977  evlslem2  21986  mpfind  22014  gsumply1subr  22118  psrplusgpropd  22120  ply1scln0  22178  evls1addd  22258  evls1muld  22259  evls1vsca  22260  asclply1subcl  22261  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  smatvscl  22411  scmatrhmcl  22415  mat1scmat  22426  smadiadetglem2  22559  cramerimplem2  22571  cramerimplem3  22572  cramerimp  22573  1pmatscmul  22589  mat2pmatf1  22616  pm2mp  22712  chmatcl  22715  chmatval  22716  chmaidscmat  22735  chfacfisf  22741  cayhamlem1  22753  cpmidgsumm2pm  22756  cpmidpmat  22760  cpmadugsumfi  22764  cpmadumatpoly  22770  cayhamlem3  22774  pptbas  22895  elcls  22960  neiint  22991  neiptopnei  23019  restbas  23045  neitr  23067  iscnp4  23150  cnconst2  23170  cnpdis  23180  cnt0  23233  cnhaus  23241  cmpcovf  23278  hauscmplem  23293  conncompid  23318  2ndci  23335  2ndc1stc  23338  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  2ndcsep  23346  dis2ndc  23347  restlly  23370  islly2  23371  lly1stc  23383  dislly  23384  finlocfin  23407  dissnlocfin  23416  locfindis  23417  llycmpkgen2  23437  ptbasfi  23468  neitx  23494  ptpjopn  23499  ptcnplem  23508  upxp  23510  txlly  23523  txtube  23527  tx1stc  23537  txkgen  23539  xkococnlem  23546  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  hmeoimaf1o  23657  reghmph  23680  nrmhmph  23681  ordthmeolem  23688  trfil2  23774  fmfnfm  23845  hauspwpwf1  23874  fclsfnflim  23914  cnextf  23953  cnextcn  23954  tmdgsum2  23983  symgtgp  23993  subgntr  23994  opnsubg  23995  ghmcnp  24002  qustgpopn  24007  tsmsf1o  24032  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  ustexsym  24103  restutop  24125  imasdsf1olem  24261  blssexps  24314  blssex  24315  ssblex  24316  imasf1oxms  24377  blcld  24393  stdbdmopn  24406  met1stc  24409  met2ndci  24410  prdsxmslem2  24417  metcnp3  24428  cfilucfil  24447  ngptgp  24524  tgioo  24684  tgqioo  24688  zdis  24705  iccpnfhmeo  24843  xrhmeo  24844  cnheibor  24854  elpi1i  24946  cmetcusp  25254  bncssbn  25274  pjthlem2  25338  ivthlem2  25353  ovolicc1  25417  ovolicc2lem3  25420  ovolicc2lem4  25421  volsup  25457  volivth  25508  vitalilem3  25511  mbflimsup  25567  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem5  25620  limcnlp  25779  limcflf  25782  limciun  25795  dvmptfsum  25879  dvcnvlem  25880  dvcvx  25925  facth1  26072  elply2  26101  plypf1  26117  coeeq  26132  aaliou3lem8  26253  ulm2  26294  mtestbdd  26314  reeff1o  26357  logbgcd1irr  26704  dcubic2  26754  quart  26771  xrlimcnp  26878  amgm  26901  harmonicbnd4  26921  perfect  27142  dchrptlem1  27175  bposlem2  27196  lgsfcl2  27214  lgsdir  27243  lgsdi  27245  lgsne0  27246  2lgslem1a1  27300  2sqmod  27347  dchrvmasumlem2  27409  chpdifbndlem2  27465  pntpbnd1  27497  pntpbnd2  27498  padicabv  27541  sltres  27574  nolesgn2o  27583  nogesgn1o  27585  nodense  27604  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  noetalem1  27653  nocvxmin  27690  noeta2  27696  onscutlt  28165  eucliddivs  28265  readdscl  28350  tgcgrxfr  28445  idmot  28464  legid  28514  btwnleg  28515  leg0  28519  tghilberti1  28564  mirreu3  28581  colperpex  28660  lnopp2hpgb  28690  axcgrrflx  28841  axsegconlem1  28844  axcontlem2  28892  axcontlem12  28902  eengtrkg  28913  wwlksnredwwlkn  29825  0wlkon  30049  0trlon  30053  upgr3v3e3cycl  30109  frgrogt3nreg  30326  nvpi  30596  nmlno0lem  30722  fh1  31547  fh2  31548  nmlnop0iALT  31924  nmopun  31943  branmfn  32034  opsqrlem1  32069  opsqrlem6  32074  mdslmd1lem1  32254  csmdsymi  32263  atom1d  32282  chirredlem2  32320  cdj1i  32362  cdj3i  32370  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  33143  archiabllem2a  33148  elrgspnlem4  33196  rloc0g  33222  rloc1r  33223  domnpropd  33227  sdrgdvcl  33249  sdrginvcl  33250  orngsqr  33282  ornglmullt  33285  orngrmullt  33286  lindssn  33349  lindfpropd  33353  ssdifidllem  33427  ssmxidllem  33444  rsprprmprmidlb  33494  rprmirredb  33503  1arithufd  33519  ply1asclunit  33543  ply1dg1rt  33548  ply1dg3rt0irred  33551  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  lsssra  33584  lindsun  33621  dimkerim  33623  fedgmullem2  33626  fldextrspunlem1  33670  fldextrspunfld  33671  irngss  33682  irngnzply1  33686  algextdeglem2  33708  algextdeglem4  33710  constrext2chnlem  33740  metideq  33883  metider  33884  pstmfval  33886  lmxrge0  33942  qqhval2  33972  qqhf  33976  qqhghm  33978  qqhrhm  33979  esumpcvgval  34068  esum2dlem  34082  esum2d  34083  sigainb  34126  insiga  34127  ddemeas  34226  imambfm  34253  dya2icoseg  34268  dya2iocnrect  34272  eulerpartlemgvv  34367  probun  34410  ballotlemfc0  34484  ballotlemfcc  34485  breprexplemc  34623  erdszelem8  35185  erdszelem9  35186  erdsze2lem2  35191  cnpconn  35217  txpconn  35219  ptpconn  35220  indispconn  35221  connpconn  35222  cvxpconn  35229  cnllysconn  35232  cvmcov2  35262  cvmopnlem  35265  cvmliftmolem1  35268  cvmliftlem14  35284  cvmliftlem15  35285  cvmlift2lem13  35302  cvmlift3lem2  35307  cvmlift3lem9  35314  seglerflx  36100  seglemin  36101  btwnsegle  36105  hilbert1.1  36142  neibastop2lem  36348  weiunfrlem  36452  weiunso  36454  bj-finsumval0  37273  relowlssretop  37351  wl-2sb6d  37546  tan2h  37606  poimirlem1  37615  poimirlem3  37617  poimirlem4  37618  poimirlem9  37623  poimirlem22  37636  poimirlem28  37642  heicant  37649  mblfinlem2  37652  itg2addnc  37668  ftc2nc  37696  dvasin  37698  sdclem1  37737  fdc  37739  istotbnd3  37765  sstotbnd  37769  prdstotbnd  37788  prdsbnd2  37789  cntotbnd  37790  rngoisocnv  37975  lsmsat  39001  islfld  39055  ps-2  39472  lplnexllnN  39558  4atlem9  39597  4atlem10a  39598  lnatexN  39773  2lnat  39778  pmapjat1  39847  lhpj1  40016  lhpm0atN  40023  4atexlemex2  40065  4atex  40070  4atex2-0aOLDN  40072  4atex2-0cOLDN  40074  lautcnvle  40083  lautj  40087  lautm  40088  idltrn  40144  cdleme01N  40215  cdleme0ex1N  40217  cdleme5  40234  cdleme9  40247  cdleme11c  40255  cdleme11g  40259  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdlemefrs32fva1  40395  cdleme32fva  40431  cdleme32fva1  40432  cdleme32fvaw  40433  cdleme32d  40438  cdleme32f  40440  cdleme35fnpq  40443  cdleme48d  40529  cdleme48gfv  40531  cdleme50ltrn  40551  trlord  40563  cdlemg4b1  40603  cdlemg4b2  40604  cdlemg13a  40645  cdlemg17a  40655  cdlemg17f  40660  erng1lem  40981  erngdvlem3  40984  erngdvlem4  40985  erng1r  40989  erngdvlem3-rN  40992  erngdvlem4-rN  40993  dva0g  41021  dialss  41040  dia0  41046  dia1N  41047  diaglbN  41049  diameetN  41050  diainN  41051  diaintclN  41052  dia1dim  41055  dia2dimlem5  41062  dia2dimlem7  41064  dia2dimlem9  41066  dia2dimlem10  41067  dia2dimlem12  41069  dia2dimlem13  41070  dvhopvadd  41087  dvhvaddass  41091  dvhopvsca  41096  tendolinv  41099  tendorinv  41100  dvhlveclem  41102  dvh0g  41105  dvheveccl  41106  dvhopN  41110  docaclN  41118  diaocN  41119  djajN  41131  dib0  41158  dib1dim  41159  dibglbN  41160  dibintclN  41161  dib1dim2  41162  diblss  41164  diblsmopel  41165  dicvaddcl  41184  dicvscacl  41185  diclspsn  41188  cdlemn4a  41193  cdlemn11c  41203  dihjustlem  41210  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2cN  41215  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihlsscpre  41228  dih1dimb  41234  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihvalcq2  41241  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dih0  41274  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetlem4preN  41300  dih1dimatlem0  41322  dih1dimatlem  41323  dihatlat  41328  dihatexv  41332  dihglb2  41336  dihmeet  41337  dihintcl  41338  dihmeet2  41340  doch2val2  41358  dochocss  41360  dihoml4c  41370  dochdmj1  41384  djhlj  41395  djhljjN  41396  djhjlj  41397  dihsumssj  41402  djhexmid  41405  djhlsmcl  41408  djhcvat42  41409  dihjatcclem4  41415  dihjat1lem  41422  dihsmsprn  41424  dihjat3  41426  dvh3dim2  41442  dvh3dim3N  41443  dochkr1OLDN  41473  lclkrlem2c  41503  lclkrlem2d  41504  mapdpglem23  41688  hdmap11lem2  41836  0prjspn  42616  mzpcompact2lem  42739  diophrw  42747  rexrabdioph  42782  eldioph4b  42799  pellexlem5  42821  pellfund14  42886  acongtr  42967  fnwe2lem3  43041  gicabl  43088  hbtlem2  43113  hbtlem4  43115  hbtlem5  43117  dgraalem  43134  aaitgo  43151  onexlimgt  43232  onexoegt  43233  oalim2cl  43278  cantnfresb  43313  onmcl  43320  tfsconcatfv  43330  tfsconcatrn  43331  ofoaid1  43347  ofoaid2  43348  ntrclsk13  44060  gneispb  44120  wessf1ornlem  45179  ltdiv23neg  45390  islptre  45617  limclner  45649  icccncfext  45885  stoweidlem1  45999  stoweidlem14  46012  stoweidlem24  46022  stoweidlem46  46044  stoweidlem57  46055  dirkercncflem2  46102  fourierdlem20  46125  fourierdlem41  46146  fourierdlem46  46150  fourierdlem48  46152  fourierdlem50  46154  fourierdlem62  46166  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem76  46180  fourierdlem79  46183  fourierdlem103  46207  fourierdlem104  46208  etransclem47  46279  m1modmmod  47359  iccpartiun  47435  reupr  47523  sqrtpwpw2p  47539  fmtnoprmfac1lem  47565  fmtnoprmfac2lem1  47567  lighneallem4a  47609  requad2  47624  perfectALTV  47724  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrimlem  47895  upgrimwlklem2  47898  upgrimwlklem3  47899  upgrimtrlslem1  47904  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrimlem  47933  grimgrtri  47948  gpgedgvtx1  48053  gpgedg2ov  48057  gpgedg2iv  48058  gsumlsscl  48368  lincsumcl  48420  lincscmcl  48421  isldepslvec2  48474  elbigo2  48541  relogbdivb  48551  blennnt2  48578  dignn0ldlem  48591  itsclc0yqsollem2  48752  inlinecirc02p  48776  lubeldm2  48944  glbeldm2  48945  lubsscl  48948  glbsscl  48949  isclatd  48971  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  uptrlem1  49199  fucofulem1  49299  fullthinc  49439