Theorem syl12anc 833

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  syl22anc  835  raaan  4519  raaanv  4520  raaan2  4523  soltmin  6136  xpdifid  6166  reuop  6291  f1dom3fv3dif  7269  f1prex  7284  cocan1  7291  fliftfun  7311  soisores  7326  soisoi  7327  isopolem  7344  f1oiso2  7351  weniso  7353  caovcld  7602  caovcomd  7605  onminex  7792  poxp2  8131  poxp3  8138  poseq  8146  tfrlem12  8391  omeulem1  8584  oaabs2  8650  omabs  8652  eldifsucnn  8665  naddcllem  8677  erov  8810  findcard2d  9168  frfi  9290  finsschain  9361  suplub2  9458  supgtoreq  9467  supisolem  9470  ordiso2  9512  ordtypelem7  9521  wemaplem2  9544  wemapsolem  9547  cantnflt  9669  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1  9686  wemapwe  9694  cnfcomlem  9696  cnfcom  9697  cnfcom3lem  9700  infxpenlem  10010  fseqenlem1  10021  dfac12lem2  10141  infpssrlem4  10303  enfin2i  10318  isf34lem7  10376  isf34lem6  10377  fin1a2lem7  10403  fin1a2lem10  10406  fin1a2lem11  10407  fin1a2lem13  10409  ttukeylem6  10511  ttukeylem7  10512  iundom2g  10537  fpwwe2lem5  10632  fpwwe2lem6  10633  fpwwe2lem8  10635  fpwwe2lem11  10638  fpwwe2  10640  canthnumlem  10645  canthwelem  10647  canthp1lem2  10650  pwfseqlem4  10659  inar1  10772  intgru  10811  distrlem4pr  11023  conjmul  11935  lediv12a  12111  recp1lt1  12116  cju  12212  gtndiv  12643  zsupss  12925  uzsupss  12928  icc0  13376  iccssioo2  13401  fzrev3  13571  ico01fl0  13788  fldiv  13829  modabs  13873  modltm1p1mod  13892  modifeq2int  13902  modsumfzodifsn  13913  seqcaopr  14009  seqf1olem1  14011  seqof2  14030  crreczi  14195  seqcoll  14429  seqcoll2  14430  hashtpg  14450  swrdccat3b  14694  01sqrexlem2  15194  resqrex  15201  abs1m  15286  isercoll  15618  zsum  15668  fsum2dlem  15720  fsumcom2  15724  fprod2dlem  15928  fprodcom2  15932  efsub  16047  bitsinv2  16388  sqgcd  16506  qredeu  16599  isprm7  16649  pcpremul  16780  pceulem  16782  pczpre  16784  pcdiv  16789  pcqmul  16790  pcqdiv  16794  pcexp  16796  pcdvdsb  16806  pcneg  16811  pcdvdstr  16813  pcgcd1  16814  pc2dvds  16816  pcz  16818  pcaddlem  16825  pcadd  16826  qexpz  16838  expnprm  16839  infpnlem2  16848  ramub2  16951  ramub1lem1  16963  setsstruct2  17111  f1ocpbllem  17474  f1ovscpbl  17476  mreexexlem3d  17594  mreexexlem4d  17595  fthi  17873  ipodrsima  18498  mgmpropd  18576  sgrppropd  18656  mndpropd  18684  grpsubpropd2  18965  f1ghm0to0  19159  symgfvne  19289  f1omvdmvd  19352  f1otrspeq  19356  pmtrdifwrdel  19394  pmtrdifwrdel2  19395  psgnunilem2  19404  psgnunilem3  19405  psgnvalii  19418  odf1  19471  lsmpropd  19586  ablnnncan  19731  gsummptshft  19845  dprdf1o  19943  pgpfac1lem3  19988  pgpfac1lem5  19990  pgpfaclem1  19992  ablfaclem2  19997  rngpropd  20068  srgbinomlem3  20122  ringpropd  20176  lmodprop2d  20678  lsspropd  20772  lmhmpropd  20828  lbspropd  20854  lbsextlem3  20918  iporthcom  21407  obslbs  21504  assapropd  21645  psrass1  21744  psrass23l  21747  psrass23  21749  mplsubrg  21783  mplmon  21809  mplmonmul  21810  mplcoe1  21811  mplbas2  21816  mplind  21850  evlslem2  21861  mpfind  21889  gsumply1subr  21976  psrplusgpropd  21978  ply1scln0  22034  scmataddcl  22238  scmatsubcl  22239  scmatmulcl  22240  smatvscl  22246  scmatrhmcl  22250  mat1scmat  22261  smadiadetglem2  22394  cramerimplem2  22406  cramerimplem3  22407  cramerimp  22408  1pmatscmul  22424  mat2pmatf1  22451  pm2mp  22547  chmatcl  22550  chmatval  22551  chmaidscmat  22570  chfacfisf  22576  cayhamlem1  22588  cpmidgsumm2pm  22591  cpmidpmat  22595  cpmadugsumfi  22599  cpmadumatpoly  22605  cayhamlem3  22609  pptbas  22731  elcls  22797  neiint  22828  neiptopnei  22856  restbas  22882  neitr  22904  iscnp4  22987  cnconst2  23007  cnpdis  23017  cnt0  23070  cnhaus  23078  cmpcovf  23115  hauscmplem  23130  conncompid  23155  2ndci  23172  2ndc1stc  23175  1stcrest  23177  2ndcctbss  23179  2ndcomap  23182  2ndcsep  23183  dis2ndc  23184  restlly  23207  islly2  23208  lly1stc  23220  dislly  23221  finlocfin  23244  dissnlocfin  23253  locfindis  23254  llycmpkgen2  23274  ptbasfi  23305  neitx  23331  ptpjopn  23336  ptcnplem  23345  upxp  23347  txlly  23360  txtube  23364  tx1stc  23374  txkgen  23376  xkococnlem  23383  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  hmeoimaf1o  23494  reghmph  23517  nrmhmph  23518  ordthmeolem  23525  trfil2  23611  fmfnfm  23682  hauspwpwf1  23711  fclsfnflim  23751  cnextf  23790  cnextcn  23791  tmdgsum2  23820  symgtgp  23830  subgntr  23831  opnsubg  23832  ghmcnp  23839  qustgpopn  23844  tsmsf1o  23869  tsmsxplem1  23877  tsmsxplem2  23878  tsmsxp  23879  ustexsym  23940  restutop  23962  imasdsf1olem  24099  blssexps  24152  blssex  24153  ssblex  24154  imasf1oxms  24218  blcld  24234  stdbdmopn  24247  met1stc  24250  met2ndci  24251  prdsxmslem2  24258  metcnp3  24269  cfilucfil  24288  ngptgp  24365  tgioo  24532  tgqioo  24536  zdis  24552  iccpnfhmeo  24690  xrhmeo  24691  cnheibor  24701  elpi1i  24793  cmetcusp  25102  bncssbn  25122  pjthlem2  25186  ivthlem2  25201  ovolicc1  25265  ovolicc2lem3  25268  ovolicc2lem4  25269  volsup  25305  volivth  25356  vitalilem3  25359  mbflimsup  25415  mbfi1fseqlem1  25465  mbfi1fseqlem3  25467  mbfi1fseqlem5  25469  limcnlp  25627  limcflf  25630  limciun  25643  dvmptfsum  25727  dvcnvlem  25728  dvcvx  25772  facth1  25917  elply2  25945  plypf1  25961  coeeq  25976  aaliou3lem8  26094  ulm2  26133  mtestbdd  26153  reeff1o  26195  logbgcd1irr  26535  dcubic2  26585  quart  26602  xrlimcnp  26709  amgm  26731  harmonicbnd4  26751  perfect  26970  dchrptlem1  27003  bposlem2  27024  lgsfcl2  27042  lgsdir  27071  lgsdi  27073  lgsne0  27074  2lgslem1a1  27128  2sqmod  27175  dchrvmasumlem2  27237  chpdifbndlem2  27293  pntpbnd1  27325  pntpbnd2  27326  padicabv  27369  sltres  27401  nolesgn2o  27410  nogesgn1o  27412  nodense  27431  nosupbnd1lem3  27449  nosupbnd1lem5  27451  nosupbnd2lem1  27454  noinfres  27461  noinfbnd1lem3  27464  noinfbnd1lem5  27466  noinfbnd2lem1  27469  noetalem1  27480  nocvxmin  27516  noeta2  27522  tgcgrxfr  28036  idmot  28055  legid  28105  btwnleg  28106  leg0  28110  tghilberti1  28155  mirreu3  28172  colperpex  28251  lnopp2hpgb  28281  axcgrrflx  28439  axsegconlem1  28442  axcontlem2  28490  axcontlem12  28500  eengtrkg  28511  wwlksnredwwlkn  29416  0wlkon  29640  0trlon  29644  upgr3v3e3cycl  29700  frgrogt3nreg  29917  nvpi  30187  nmlno0lem  30313  fh1  31138  fh2  31139  nmlnop0iALT  31515  nmopun  31534  branmfn  31625  opsqrlem1  31660  opsqrlem6  31665  mdslmd1lem1  31845  csmdsymi  31854  atom1d  31873  chirredlem2  31911  cdj1i  31953  cdj3i  31961  fcnvgreu  32165  suppovss  32173  xrofsup  32247  nn0difffzod  32283  pwrssmgc  32437  gsummpt2d  32471  gsumhashmul  32478  odpmco  32517  cycpmco2lem6  32560  cycpmco2  32562  cyc3evpm  32579  cycpmconjslem2  32584  archirngz  32605  archiabllem2a  32610  sdrgdvcl  32667  sdrginvcl  32668  orngsqr  32692  ornglmullt  32695  orngrmullt  32696  lindssn  32768  lindfpropd  32772  ghmqusker  32806  ssmxidllem  32863  evls1addd  32922  evls1muld  32923  evls1vsca  32924  ply1asclunit  32928  asclply1subcl  32934  ply1degltel  32940  ply1degleel  32941  ply1degltlss  32942  lsssra  32963  lindsun  32998  dimkerim  33000  fedgmullem2  33003  irngss  33040  irngnzply1  33044  algextdeglem2  33063  algextdeglem4  33065  metideq  33171  metider  33172  pstmfval  33174  lmxrge0  33230  qqhval2  33260  qqhf  33264  qqhghm  33266  qqhrhm  33267  esumpcvgval  33374  esum2dlem  33388  esum2d  33389  sigainb  33432  insiga  33433  ddemeas  33532  imambfm  33559  dya2icoseg  33574  dya2iocnrect  33578  eulerpartlemgvv  33673  probun  33716  ballotlemfc0  33789  ballotlemfcc  33790  sgnmul  33839  breprexplemc  33942  erdszelem8  34487  erdszelem9  34488  erdsze2lem2  34493  cnpconn  34519  txpconn  34521  ptpconn  34522  indispconn  34523  connpconn  34524  cvxpconn  34531  cnllysconn  34534  cvmcov2  34564  cvmopnlem  34567  cvmliftmolem1  34570  cvmliftlem14  34586  cvmliftlem15  34587  cvmlift2lem13  34604  cvmlift3lem2  34609  cvmlift3lem9  34616  seglerflx  35388  seglemin  35389  btwnsegle  35393  hilbert1.1  35430  neibastop2lem  35548  bj-finsumval0  36469  relowlssretop  36547  wl-2sb6d  36726  tan2h  36783  poimirlem1  36792  poimirlem3  36794  poimirlem4  36795  poimirlem9  36800  poimirlem22  36813  poimirlem28  36819  heicant  36826  mblfinlem2  36829  itg2addnc  36845  ftc2nc  36873  dvasin  36875  sdclem1  36914  fdc  36916  istotbnd3  36942  sstotbnd  36946  prdstotbnd  36965  prdsbnd2  36966  cntotbnd  36967  rngoisocnv  37152  lsmsat  38181  islfld  38235  ps-2  38652  lplnexllnN  38738  4atlem9  38777  4atlem10a  38778  lnatexN  38953  2lnat  38958  pmapjat1  39027  lhpj1  39196  lhpm0atN  39203  4atexlemex2  39245  4atex  39250  4atex2-0aOLDN  39252  4atex2-0cOLDN  39254  lautcnvle  39263  lautj  39267  lautm  39268  idltrn  39324  cdleme01N  39395  cdleme0ex1N  39397  cdleme5  39414  cdleme9  39427  cdleme11c  39435  cdleme11g  39439  cdlemefrs29bpre0  39570  cdlemefrs29cpre1  39572  cdlemefrs32fva1  39575  cdleme32fva  39611  cdleme32fva1  39612  cdleme32fvaw  39613  cdleme32d  39618  cdleme32f  39620  cdleme35fnpq  39623  cdleme48d  39709  cdleme48gfv  39711  cdleme50ltrn  39731  trlord  39743  cdlemg4b1  39783  cdlemg4b2  39784  cdlemg13a  39825  cdlemg17a  39835  cdlemg17f  39840  erng1lem  40161  erngdvlem3  40164  erngdvlem4  40165  erng1r  40169  erngdvlem3-rN  40172  erngdvlem4-rN  40173  dva0g  40201  dialss  40220  dia0  40226  dia1N  40227  diaglbN  40229  diameetN  40230  diainN  40231  diaintclN  40232  dia1dim  40235  dia2dimlem5  40242  dia2dimlem7  40244  dia2dimlem9  40246  dia2dimlem10  40247  dia2dimlem12  40249  dia2dimlem13  40250  dvhopvadd  40267  dvhvaddass  40271  dvhopvsca  40276  tendolinv  40279  tendorinv  40280  dvhlveclem  40282  dvh0g  40285  dvheveccl  40286  dvhopN  40290  docaclN  40298  diaocN  40299  djajN  40311  dib0  40338  dib1dim  40339  dibglbN  40340  dibintclN  40341  dib1dim2  40342  diblss  40344  diblsmopel  40345  dicvaddcl  40364  dicvscacl  40365  diclspsn  40368  cdlemn4a  40373  cdlemn11c  40383  dihjustlem  40390  dihord1  40392  dihord2a  40393  dihord2b  40394  dihord2cN  40395  dihord11b  40396  dihord11c  40398  dihord2pre  40399  dihlsscpre  40408  dih1dimb  40414  dib2dim  40417  dih2dimb  40418  dih2dimbALTN  40419  dihvalcq2  40421  dihopelvalcpre  40422  dihord6apre  40430  dihord5b  40433  dihord5apre  40436  dih0  40454  dihmeetlem1N  40464  dihglblem5apreN  40465  dihglblem3N  40469  dihmeetlem2N  40473  dihglbcpreN  40474  dihmeetlem4preN  40480  dih1dimatlem0  40502  dih1dimatlem  40503  dihatlat  40508  dihatexv  40512  dihglb2  40516  dihmeet  40517  dihintcl  40518  dihmeet2  40520  doch2val2  40538  dochocss  40540  dihoml4c  40550  dochdmj1  40564  djhlj  40575  djhljjN  40576  djhjlj  40577  dihsumssj  40582  djhexmid  40585  djhlsmcl  40588  djhcvat42  40589  dihjatcclem4  40595  dihjat1lem  40602  dihsmsprn  40604  dihjat3  40606  dvh3dim2  40622  dvh3dim3N  40623  dochkr1OLDN  40653  lclkrlem2c  40683  lclkrlem2d  40684  mapdpglem23  40868  hdmap11lem2  41016  expgcd  41527  0prjspn  41672  mzpcompact2lem  41791  diophrw  41799  rexrabdioph  41834  eldioph4b  41851  pellexlem5  41873  pellfund14  41938  acongtr  42019  fnwe2lem3  42096  gicabl  42143  hbtlem2  42168  hbtlem4  42170  hbtlem5  42172  dgraalem  42189  aaitgo  42206  onexlimgt  42294  onexoegt  42295  oalim2cl  42341  cantnfresb  42376  onmcl  42383  tfsconcatfv  42393  tfsconcatrn  42394  ofoaid1  42410  ofoaid2  42411  ntrclsk13  43124  gneispb  43184  wessf1ornlem  44182  ltdiv23neg  44402  islptre  44633  limclner  44665  icccncfext  44901  stoweidlem1  45015  stoweidlem14  45028  stoweidlem24  45038  stoweidlem46  45060  stoweidlem57  45071  dirkercncflem2  45118  fourierdlem20  45141  fourierdlem41  45162  fourierdlem46  45166  fourierdlem48  45168  fourierdlem50  45170  fourierdlem62  45182  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem76  45196  fourierdlem79  45199  fourierdlem103  45223  fourierdlem104  45224  etransclem47  45295  iccpartiun  46400  reupr  46488  sqrtpwpw2p  46504  fmtnoprmfac1lem  46530  fmtnoprmfac2lem1  46532  lighneallem4a  46574  requad2  46589  perfectALTV  46689  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  gsumlsscl  47147  lincsumcl  47199  lincscmcl  47200  isldepslvec2  47253  m1modmmod  47294  elbigo2  47325  relogbdivb  47335  blennnt2  47362  dignn0ldlem  47375  itsclc0yqsollem2  47536  inlinecirc02p  47560  lubeldm2  47676  glbeldm2  47677  lubsscl  47680  glbsscl  47681  isclatd  47695  fullthinc  47753