Theorem syl12anc 850

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl22anc  852  raaan  4477  raaanv  4478  raaan2  4481  copsex2dv  5473  soltmin  6148  xpdifid  6177  xpdifcnvepel  6178  reuop  6322  f1dom3fv3dif  7303  f1prex  7323  cocan1  7330  fliftfun  7351  soisores  7366  soisoi  7367  isopolem  7384  f1oiso2  7391  weniso  7395  caovcld  7646  caovcomd  7649  onminex  7850  fnwe2lem4  8185  poxp2  8197  poxp3  8204  poseq  8212  tfrlem12  8435  omeulem1  8628  nnaordex2  8686  oaabs2  8696  omabs  8698  eldifsucnn  8711  naddcllem  8723  erov  8873  findcard2d  9220  frfi  9314  finsschain  9386  suplub2  9490  supgtoreq  9500  supisolem  9503  ordiso2  9546  ordtypelem7  9555  wemaplem2  9578  wemapsolem  9581  cantnflt  9710  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1  9727  wemapwe  9735  cnfcomlem  9737  cnfcom  9738  cnfcom3lem  9741  infxpenlem  10131  fseqenlem1  10142  dfac12lem2  10262  infpssrlem4  10423  enfin2i  10438  isf34lem7  10496  isf34lem6  10497  fin1a2lem7  10523  fin1a2lem10  10526  fin1a2lem11  10527  fin1a2lem13  10529  ttukeylem6  10631  ttukeylem7  10632  iundom2g  10663  fpwwe2lem5  10759  fpwwe2lem6  10760  fpwwe2lem8  10762  fpwwe2lem11  10765  fpwwe2  10767  canthnumlem  10772  canthwelem  10774  canthp1lem2  10777  pwfseqlem4  10786  inar1  10899  intgru  10938  distrlem4pr  11150  conjmul  12074  lediv12a  12250  recp1lt1  12255  cju  12356  gtndiv  12816  zsupss  13104  uzsupss  13107  icc0  13564  iccssioo2  13590  fzrev3  13764  ico01fl0  13999  fldiv  14040  modabs  14084  modltm1p1mod  14106  modifeq2int  14116  modsumfzodifsn  14127  seqcaopr  14222  seqf1olem1  14224  seqof2  14243  crreczi  14413  seqcoll  14650  seqcoll2  14651  hashtpg  14671  swrdccat3b  14931  sgnmul  15303  01sqrexlem2  15453  resqrex  15460  abs1m  15546  isercoll  15879  zsum  15928  fsum2dlem  15980  fsumcom2  15984  fprod2dlem  16191  fprodcom2  16195  efsub  16312  bitsinv2  16657  sqgcd  16780  expgcd  16781  qredeu  16877  isprm7  16928  pcpremul  17065  pceulem  17067  pczpre  17069  pcdiv  17074  pcqmul  17075  pcqdiv  17079  pcexp  17081  pcdvdsb  17091  pcneg  17096  pcdvdstr  17098  pcgcd1  17099  pc2dvds  17101  pcz  17103  pcaddlem  17110  pcadd  17111  qexpz  17123  expnprm  17124  infpnlem2  17133  ramub2  17236  ramub1lem1  17248  setsstruct2  17396  f1ocpbllem  17746  f1ovscpbl  17748  mreexexlem3d  17870  mreexexlem4d  17871  fthi  18145  ipodrsima  18765  chnind  18845  mgmpropd  18879  sgrppropd  18970  mndpropd  19001  grpsubpropd2  19306  f1ghm0to0  19509  ghmqusker  19552  symgfvne  19646  f1omvdmvd  19708  f1otrspeq  19712  pmtrdifwrdel  19750  pmtrdifwrdel2  19751  psgnunilem2  19760  psgnunilem3  19761  psgnvalii  19774  odf1  19827  lsmpropd  19942  ablnnncan  20087  gsummptshft  20201  dprdf1o  20299  pgpfac1lem3  20344  pgpfac1lem5  20346  pgpfaclem1  20348  ablfaclem2  20353  rngpropd  20447  srgbinomlem3  20505  ringpropd  20570  orngsqr  21174  ornglmullt  21177  orngrmullt  21178  lmodprop2d  21250  lsspropd  21343  lmhmpropd  21399  lbspropd  21425  lbsextlem3  21489  unichnlidl  21567  ssdifidllem  21691  iporthcom  21996  obslbs  22091  assapropd  22234  psrass1  22326  psrass23l  22329  psrass23  22331  mplsubrg  22367  mplmon  22399  mplmonmul  22400  mplcoe1  22401  mplbas2  22406  mplind  22434  evlslem2  22443  mpfind  22479  gsumply1subr  22606  psrplusgpropd  22608  ply1scln0  22665  evls1addd  22744  evls1muld  22745  evls1vsca  22746  asclply1subcl  22747  scmataddcl  22886  scmatsubcl  22887  scmatmulcl  22888  smatvscl  22894  scmatrhmcl  22898  mat1scmat  22909  smadiadetglem2  23042  cramerimplem2  23057  cramerimplem3  23058  cramerimp  23059  1pmatscmul  23075  mat2pmatf1  23102  pm2mp  23198  chmatcl  23201  chmatval  23202  chmaidscmat  23221  chfacfisf  23227  cayhamlem1  23239  cpmidgsumm2pm  23242  cpmidpmat  23246  cpmadugsumfi  23250  cpmadumatpoly  23256  cayhamlem3  23260  pptbas  23381  elcls  23446  neiint  23477  neiptopnei  23505  restbas  23531  neitr  23553  iscnp4  23636  cnconst2  23656  cnpdis  23666  cnt0  23719  cnhaus  23727  cmpcovf  23764  hauscmplem  23779  conncompid  23804  2ndci  23821  2ndc1stc  23824  1stcrest  23826  2ndcctbss  23829  2ndcomap  23832  2ndcsep  23833  dis2ndc  23834  restlly  23857  islly2  23858  lly1stc  23870  dislly  23871  finlocfin  23894  dissnlocfin  23903  locfindis  23904  llycmpkgen2  23924  ptbasfi  23955  neitx  23981  ptpjopn  23986  ptcnplem  23995  upxp  23997  txlly  24010  txtube  24014  tx1stc  24024  txkgen  24026  xkococnlem  24033  kqreglem1  24115  kqreglem2  24116  kqnrmlem1  24117  kqnrmlem2  24118  hmeoimaf1o  24144  reghmph  24167  nrmhmph  24168  ordthmeolem  24175  trfil2  24261  fmfnfm  24332  hauspwpwf1  24361  fclsfnflim  24401  cnextf  24440  cnextcn  24441  tmdgsum2  24470  symgtgp  24480  subgntr  24481  opnsubg  24482  ghmcnp  24489  qustgpopn  24494  tsmsf1o  24519  tsmsxplem1  24527  tsmsxplem2  24528  tsmsxp  24529  ustexsym  24590  restutop  24611  imasdsf1olem  24747  blssexps  24800  blssex  24801  ssblex  24802  imasf1oxms  24863  blcld  24879  stdbdmopn  24892  met1stc  24895  met2ndci  24896  prdsxmslem2  24903  metcnp3  24914  cfilucfil  24933  ngptgp  25010  tgioo  25170  tgqioo  25174  zdis  25191  iccpnfhmeo  25321  xrhmeo  25322  cnheibor  25331  elpi1i  25422  cmetcusp  25730  bncssbn  25750  pjthlem2  25814  ivthlem2  25828  ovolicc1  25892  ovolicc2lem3  25895  ovolicc2lem4  25896  volsup  25932  volivth  25983  vitalilem3  25986  mbflimsup  26042  mbfi1fseqlem1  26091  mbfi1fseqlem3  26093  mbfi1fseqlem5  26095  limcnlp  26253  limcflf  26256  limciun  26269  dvmptfsum  26350  dvcnvlem  26351  dvcvx  26395  facth1  26540  elply2  26569  plypf1  26586  coeeq  26601  aaliou3lem8  26729  ulm2  26769  mtestbdd  26789  reeff1o  26831  logbgcd1irr  27179  dcubic2  27229  quart  27246  xrlimcnp  27353  amgm  27375  harmonicbnd4  27395  perfect  27615  dchrptlem1  27648  bposlem2  27669  lgsfcl2  27687  lgsdir  27716  lgsdi  27718  lgsne0  27719  2lgslem1a1  27773  2sqmod  27820  dchrvmasumlem2  27882  chpdifbndlem2  27938  pntpbnd1  27970  pntpbnd2  27971  padicabv  28014  ltsres  28076  nolesgn2o  28085  nogesgn1o  28087  nodense  28106  nosupbnd1lem3  28124  nosupbnd1lem5  28126  nosupbnd2lem1  28129  noinfres  28136  noinfbnd1lem3  28139  noinfbnd1lem5  28141  noinfbnd2lem1  28144  noetalem1  28155  nocvxmin  28198  noeta2  28204  oncutlt  28707  eucliddivs  28819  readdscl  28942  tgcgrxfr  29038  idmot  29057  legid  29107  btwnleg  29108  leg0  29112  tghilberti1  29162  mirreu3  29183  colperpex  29266  lnopp2hpgb  29298  dfprlng2  29482  axcgrrflx  29549  axsegconlem1  29552  axcontlem2  29600  axcontlem12  29610  eengtrkg  29621  wwlksnredwwlkn  30541  0wlkon  30768  0trlon  30772  upgr3v3e3cycl  30838  frgrogt3nreg  31055  nvpi  31326  nmlno0lem  31452  fh1  32277  fh2  32278  nmlnop0iALT  32654  nmopun  32673  branmfn  32764  opsqrlem1  32799  opsqrlem6  32804  mdslmd1lem1  32984  csmdsymi  32993  atom1d  33012  chirredlem2  33050  cdj1i  33092  cdj3i  33100  fcnvgreu  33364  suppovss  33371  xrofsup  33455  nn0difffzod  33492  pwrssmgc  33660  gsummpt2d  33709  gsumhashmul  33727  odpmco  33746  cycpmco2lem6  33791  cycpmco2  33793  cyc3evpm  33810  cycpmconjslem2  33815  fxpsubg  33833  fxpsdrg  33835  archirngz  33849  archiabllem2a  33854  elrgspnlem4  33905  rloc0g  33932  rloc1r  33933  domnpropd  33940  sdrgdvcl  33965  sdrginvcl  33966  lindssn  34037  lindfpropd  34041  ssmxidllem  34102  drnglring  34128  dflring2  34129  rsprprmprmidlb  34159  rprmirredb  34168  1arithufd  34184  ply1asclunit  34209  ply1dg1rt  34215  ply1dg3rt0irred  34219  ply1degltel  34229  ply1degleel  34230  ply1degltlss  34231  psrmonmul  34293  esplyind  34318  esplyindfv  34319  lsssra  34331  lindsun  34368  dimkerim  34370  fedgmullem2  34373  fldextrspunlem1  34418  fldextrspunfld  34419  irngss  34430  irngnzply1  34434  algextdeglem2  34461  algextdeglem4  34463  constrext2chnlem  34493  metideq  34636  metider  34637  pstmfval  34639  lmxrge0  34695  qqhval2  34725  qqhf  34729  qqhghm  34731  qqhrhm  34732  esumpcvgval  34821  esum2dlem  34835  esum2d  34836  sigainb  34880  insiga  34881  ddemeas  34980  imambfm  35005  dya2icoseg  35020  dya2iocnrect  35024  eulerpartlemgvv  35119  probun  35162  ballotlemfc0  35236  ballotlemfcc  35237  breprexplemc  35372  omeueq  35837  erdszelem8  36171  erdszelem9  36172  erdsze2lem2  36177  cnpconn  36203  txpconn  36205  ptpconn  36206  indispconn  36207  connpconn  36208  cvxpconn  36215  cnllysconn  36218  cvmcov2  36248  cvmopnlem  36251  cvmliftmolem1  36254  cvmliftlem14  36270  cvmliftlem15  36271  cvmlift2lem13  36288  cvmlift3lem2  36293  cvmlift3lem9  36300  seglerflx  37092  seglemin  37093  btwnsegle  37097  hilbert1.1  37134  neibastop2lem  37363  weiunfrlem  37467  weiunso  37469  mh-inf3f1  37544  bj-finsumval0  38474  qdiff  38516  relowlssretop  38554  wl-2sb6d  38758  tan2h  38803  poimirlem1  38807  poimirlem3  38809  poimirlem4  38810  poimirlem9  38815  poimirlem22  38828  poimirlem28  38834  heicant  38841  mblfinlem2  38844  itg2addnc  38860  ftc2nc  38888  dvasin  38890  sdclem1  38943  fdc  38945  istotbnd3  38971  sstotbnd  38975  prdstotbnd  38994  prdsbnd2  38995  cntotbnd  38996  rngoisocnv  39181  lsmsat  40331  islfld  40385  ps-2  40801  lplnexllnN  40887  4atlem9  40926  4atlem10a  40927  lnatexN  41102  2lnat  41107  pmapjat1  41176  lhpj1  41345  lhpm0atN  41352  4atexlemex2  41394  4atex  41399  4atex2-0aOLDN  41401  4atex2-0cOLDN  41403  lautcnvle  41412  lautj  41416  lautm  41417  idltrn  41473  cdleme01N  41544  cdleme0ex1N  41546  cdleme5  41563  cdleme9  41576  cdleme11c  41584  cdleme11g  41588  cdlemefrs29bpre0  41719  cdlemefrs29cpre1  41721  cdlemefrs32fva1  41724  cdleme32fva  41760  cdleme32fva1  41761  cdleme32fvaw  41762  cdleme32d  41767  cdleme32f  41769  cdleme35fnpq  41772  cdleme48d  41858  cdleme48gfv  41860  cdleme50ltrn  41880  trlord  41892  cdlemg4b1  41932  cdlemg4b2  41933  cdlemg13a  41974  cdlemg17a  41984  cdlemg17f  41989  erng1lem  42310  erngdvlem3  42313  erngdvlem4  42314  erng1r  42318  erngdvlem3-rN  42321  erngdvlem4-rN  42322  dva0g  42350  dialss  42369  dia0  42375  dia1N  42376  diaglbN  42378  diameetN  42379  diainN  42380  diaintclN  42381  dia1dim  42384  dia2dimlem5  42391  dia2dimlem7  42393  dia2dimlem9  42395  dia2dimlem10  42396  dia2dimlem12  42398  dia2dimlem13  42399  dvhopvadd  42416  dvhvaddass  42420  dvhopvsca  42425  tendolinv  42428  tendorinv  42429  dvhlveclem  42431  dvh0g  42434  dvheveccl  42435  dvhopN  42439  docaclN  42447  diaocN  42448  djajN  42460  dib0  42487  dib1dim  42488  dibglbN  42489  dibintclN  42490  dib1dim2  42491  diblss  42493  diblsmopel  42494  dicvaddcl  42513  dicvscacl  42514  diclspsn  42517  cdlemn4a  42522  cdlemn11c  42532  dihjustlem  42539  dihord1  42541  dihord2a  42542  dihord2b  42543  dihord2cN  42544  dihord11b  42545  dihord11c  42547  dihord2pre  42548  dihlsscpre  42557  dih1dimb  42563  dib2dim  42566  dih2dimb  42567  dih2dimbALTN  42568  dihvalcq2  42570  dihopelvalcpre  42571  dihord6apre  42579  dihord5b  42582  dihord5apre  42585  dih0  42603  dihmeetlem1N  42613  dihglblem5apreN  42614  dihglblem3N  42618  dihmeetlem2N  42622  dihglbcpreN  42623  dihmeetlem4preN  42629  dih1dimatlem0  42651  dih1dimatlem  42652  dihatlat  42657  dihatexv  42661  dihglb2  42665  dihmeet  42666  dihintcl  42667  dihmeet2  42669  doch2val2  42687  dochocss  42689  dihoml4c  42699  dochdmj1  42713  djhlj  42724  djhljjN  42725  djhjlj  42726  dihsumssj  42731  djhexmid  42734  djhlsmcl  42737  djhcvat42  42738  dihjatcclem4  42744  dihjat1lem  42751  dihsmsprn  42753  dihjat3  42755  dvh3dim2  42771  dvh3dim3N  42772  dochkr1OLDN  42802  lclkrlem2c  42832  lclkrlem2d  42833  mapdpglem23  43017  hdmap11lem2  43165  0prjspn  43930  mzpcompact2lem  44028  diophrw  44036  rexrabdioph  44067  eldioph4b  44084  pellexlem5  44106  pellfund14  44171  acongtr  44251  gicabl  44367  hbtlem2  44391  hbtlem4  44393  hbtlem5  44395  dgraalem  44412  aaitgo  44429  onexlimgt  44506  onexoegt  44507  oalim2cl  44552  cantnfresb  44587  onmcl  44594  tfsconcatfv  44604  tfsconcatrn  44605  ofoaid1  44621  ofoaid2  44622  ntrclsk13  45332  gneispb  45392  wessf1ornlem  46473  ltdiv23neg  46678  islptre  46904  limclner  46934  icccncfext  47170  stoweidlem1  47284  stoweidlem14  47297  stoweidlem24  47307  stoweidlem46  47329  stoweidlem57  47340  dirkercncflem2  47387  fourierdlem20  47410  fourierdlem41  47431  fourierdlem46  47435  fourierdlem48  47437  fourierdlem50  47439  fourierdlem62  47451  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem76  47465  fourierdlem79  47468  fourierdlem103  47492  fourierdlem104  47493  etransclem47  47564  m1modmmod  48707  iccpartiun  48789  reupr  48877  sqrtpwpw2p  48896  fmtnoprmfac1lem  48922  fmtnoprmfac2lem1  48924  lighneallem4a  48966  requad2  48994  perfectALTV  49094  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  isuspgrim0lem  49264  isuspgrim0  49265  isuspgrimlem  49266  upgrimwlklem2  49269  upgrimwlklem3  49270  upgrimtrlslem1  49275  uhgrimisgrgriclem  49301  uhgrimisgrgric  49302  clnbgrgrimlem  49304  grimgrtri  49320  gpgedgvtx1  49433  gpgedg2ov  49437  gpgedg2iv  49438  gsumlsscl  49823  lincsumcl  49874  lincscmcl  49875  isldepslvec2  49928  elbigo2  49995  relogbdivb  50005  blennnt2  50032  dignn0ldlem  50045  itsclc0yqsollem2  50206  inlinecirc02p  50230  lubeldm2  50401  glbeldm2  50402  lubsscl  50405  glbsscl  50406  isclatd  50428  sectpropdlem  50481  invpropdlem  50483  isopropdlem  50485  uptrlem1  50657  fucofulem1  50763  fullthinc  50916