Theorem syl12anc 835

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  837  raaan  4457  raaanv  4458  raaan2  4461  soltmin  6056  xpdifid  6086  reuop  6211  f1dom3fv3dif  7173  f1prex  7188  cocan1  7195  fliftfun  7215  soisores  7230  soisoi  7231  isopolem  7248  f1oiso2  7255  weniso  7257  caovcld  7497  caovcomd  7500  onminex  7684  tfrlem12  8251  omeulem1  8444  oaabs2  8510  omabs  8512  eldifsucnn  8525  erov  8634  findcard2d  8987  frfi  9103  finsschain  9170  suplub2  9264  supgtoreq  9273  supisolem  9276  ordiso2  9318  ordtypelem7  9327  wemaplem2  9350  wemapsolem  9353  cantnflt  9474  cantnfp1lem3  9482  cantnflem1b  9488  cantnflem1  9491  wemapwe  9499  cnfcomlem  9501  cnfcom  9502  cnfcom3lem  9505  infxpenlem  9815  fseqenlem1  9826  dfac12lem2  9946  infpssrlem4  10108  enfin2i  10123  isf34lem7  10181  isf34lem6  10182  fin1a2lem7  10208  fin1a2lem10  10211  fin1a2lem11  10212  fin1a2lem13  10214  ttukeylem6  10316  ttukeylem7  10317  iundom2g  10342  fpwwe2lem5  10437  fpwwe2lem6  10438  fpwwe2lem8  10440  fpwwe2lem11  10443  fpwwe2  10445  canthnumlem  10450  canthwelem  10452  canthp1lem2  10455  pwfseqlem4  10464  inar1  10577  intgru  10616  distrlem4pr  10828  conjmul  11738  lediv12a  11914  recp1lt1  11919  cju  12015  gtndiv  12443  zsupss  12723  uzsupss  12726  icc0  13173  iccssioo2  13198  fzrev3  13368  ico01fl0  13585  fldiv  13626  modabs  13670  modltm1p1mod  13689  modifeq2int  13699  modsumfzodifsn  13710  seqcaopr  13806  seqf1olem1  13808  seqof2  13827  crreczi  13989  seqcoll  14223  seqcoll2  14224  hashtpg  14244  swrdccat3b  14498  sqrlem2  15000  resqrex  15007  abs1m  15092  isercoll  15424  zsum  15475  fsum2dlem  15527  fsumcom2  15531  fprod2dlem  15735  fprodcom2  15739  efsub  15854  bitsinv2  16195  sqgcd  16315  qredeu  16408  isprm7  16458  pcpremul  16589  pceulem  16591  pczpre  16593  pcdiv  16598  pcqmul  16599  pcqdiv  16603  pcexp  16605  pcdvdsb  16615  pcneg  16620  pcdvdstr  16622  pcgcd1  16623  pc2dvds  16625  pcz  16627  pcaddlem  16634  pcadd  16635  qexpz  16647  expnprm  16648  infpnlem2  16657  ramub2  16760  ramub1lem1  16772  setsstruct2  16920  f1ocpbllem  17280  f1ovscpbl  17282  mreexexlem3d  17400  mreexexlem4d  17401  fthi  17679  ipodrsima  18304  mndpropd  18455  grpsubpropd2  18726  ghmf1  18908  symgfvne  19033  f1omvdmvd  19096  f1otrspeq  19100  pmtrdifwrdel  19138  pmtrdifwrdel2  19139  psgnunilem2  19148  psgnunilem3  19149  psgnvalii  19162  odf1  19214  lsmpropd  19328  ablnnncan  19469  gsummptshft  19582  dprdf1o  19680  pgpfac1lem3  19725  pgpfac1lem5  19727  pgpfaclem1  19729  ablfaclem2  19734  srgbinomlem3  19823  ringpropd  19866  f1ghm0to0  20029  lmodprop2d  20230  lsspropd  20324  lmhmpropd  20380  lbspropd  20406  lbsextlem3  20467  iporthcom  20885  obslbs  20982  assapropd  21121  psrass1  21219  psrass23l  21222  psrass23  21224  mplsubrg  21256  mplmon  21281  mplmonmul  21282  mplcoe1  21283  mplbas2  21288  mplind  21323  evlslem2  21334  mpfind  21362  gsumply1subr  21450  psrplusgpropd  21452  ply1scln0  21507  scmataddcl  21710  scmatsubcl  21711  scmatmulcl  21712  smatvscl  21718  scmatrhmcl  21722  mat1scmat  21733  smadiadetglem2  21866  cramerimplem2  21878  cramerimplem3  21879  cramerimp  21880  1pmatscmul  21896  mat2pmatf1  21923  pm2mp  22019  chmatcl  22022  chmatval  22023  chmaidscmat  22042  chfacfisf  22048  cayhamlem1  22060  cpmidgsumm2pm  22063  cpmidpmat  22067  cpmadugsumfi  22071  cpmadumatpoly  22077  cayhamlem3  22081  pptbas  22203  elcls  22269  neiint  22300  neiptopnei  22328  restbas  22354  neitr  22376  iscnp4  22459  cnconst2  22479  cnpdis  22489  cnt0  22542  cnhaus  22550  cmpcovf  22587  hauscmplem  22602  conncompid  22627  2ndci  22644  2ndc1stc  22647  1stcrest  22649  2ndcctbss  22651  2ndcomap  22654  2ndcsep  22655  dis2ndc  22656  restlly  22679  islly2  22680  lly1stc  22692  dislly  22693  finlocfin  22716  dissnlocfin  22725  locfindis  22726  llycmpkgen2  22746  ptbasfi  22777  neitx  22803  ptpjopn  22808  ptcnplem  22817  upxp  22819  txlly  22832  txtube  22836  tx1stc  22846  txkgen  22848  xkococnlem  22855  kqreglem1  22937  kqreglem2  22938  kqnrmlem1  22939  kqnrmlem2  22940  hmeoimaf1o  22966  reghmph  22989  nrmhmph  22990  ordthmeolem  22997  trfil2  23083  fmfnfm  23154  hauspwpwf1  23183  fclsfnflim  23223  cnextf  23262  cnextcn  23263  tmdgsum2  23292  symgtgp  23302  subgntr  23303  opnsubg  23304  ghmcnp  23311  qustgpopn  23316  tsmsf1o  23341  tsmsxplem1  23349  tsmsxplem2  23350  tsmsxp  23351  ustexsym  23412  restutop  23434  imasdsf1olem  23571  blssexps  23624  blssex  23625  ssblex  23626  imasf1oxms  23690  blcld  23706  stdbdmopn  23719  met1stc  23722  met2ndci  23723  prdsxmslem2  23730  metcnp3  23741  cfilucfil  23760  ngptgp  23837  tgioo  24004  tgqioo  24008  zdis  24024  iccpnfhmeo  24153  xrhmeo  24154  cnheibor  24163  elpi1i  24254  cmetcusp  24563  bncssbn  24583  pjthlem2  24647  ivthlem2  24661  ovolicc1  24725  ovolicc2lem3  24728  ovolicc2lem4  24729  volsup  24765  volivth  24816  vitalilem3  24819  mbflimsup  24875  mbfi1fseqlem1  24925  mbfi1fseqlem3  24927  mbfi1fseqlem5  24929  limcnlp  25087  limcflf  25090  limciun  25103  dvmptfsum  25184  dvcnvlem  25185  dvcvx  25229  facth1  25374  elply2  25402  plypf1  25418  coeeq  25433  aaliou3lem8  25550  ulm2  25589  mtestbdd  25609  reeff1o  25651  logbgcd1irr  25989  dcubic2  26039  quart  26056  xrlimcnp  26163  amgm  26185  harmonicbnd4  26205  perfect  26424  dchrptlem1  26457  bposlem2  26478  lgsfcl2  26496  lgsdir  26525  lgsdi  26527  lgsne0  26528  2lgslem1a1  26582  2sqmod  26629  dchrvmasumlem2  26691  chpdifbndlem2  26747  pntpbnd1  26779  pntpbnd2  26780  padicabv  26823  tgcgrxfr  26924  idmot  26943  legid  26993  btwnleg  26994  leg0  26998  tghilberti1  27043  mirreu3  27060  colperpex  27139  lnopp2hpgb  27169  axcgrrflx  27327  axsegconlem1  27330  axcontlem2  27378  axcontlem12  27388  eengtrkg  27399  wwlksnredwwlkn  28305  0wlkon  28529  0trlon  28533  upgr3v3e3cycl  28589  frgrogt3nreg  28806  nvpi  29074  nmlno0lem  29200  fh1  30025  fh2  30026  nmlnop0iALT  30402  nmopun  30421  branmfn  30512  opsqrlem1  30547  opsqrlem6  30552  mdslmd1lem1  30732  csmdsymi  30741  atom1d  30760  chirredlem2  30798  cdj1i  30840  cdj3i  30848  fcnvgreu  31055  suppovss  31062  xrofsup  31135  pwrssmgc  31323  gsummpt2d  31354  gsumhashmul  31361  odpmco  31400  cycpmco2lem6  31443  cycpmco2  31445  cyc3evpm  31462  cycpmconjslem2  31467  archirngz  31488  archiabllem2a  31493  orngsqr  31548  ornglmullt  31551  orngrmullt  31552  lindssn  31618  lindfpropd  31621  ssmxidllem  31686  lindsun  31751  dimkerim  31753  fedgmullem2  31756  metideq  31888  metider  31889  pstmfval  31891  lmxrge0  31947  qqhval2  31977  qqhf  31981  qqhghm  31983  qqhrhm  31984  esumpcvgval  32091  esum2dlem  32105  esum2d  32106  sigainb  32149  insiga  32150  ddemeas  32249  imambfm  32274  dya2icoseg  32289  dya2iocnrect  32293  eulerpartlemgvv  32388  probun  32431  ballotlemfc0  32504  ballotlemfcc  32505  sgnmul  32554  breprexplemc  32657  erdszelem8  33205  erdszelem9  33206  erdsze2lem2  33211  cnpconn  33237  txpconn  33239  ptpconn  33240  indispconn  33241  connpconn  33242  cvxpconn  33249  cnllysconn  33252  cvmcov2  33282  cvmopnlem  33285  cvmliftmolem1  33288  cvmliftlem14  33304  cvmliftlem15  33305  cvmlift2lem13  33322  cvmlift3lem2  33327  cvmlift3lem9  33334  poxp2  33835  poxp3  33841  poseq  33847  naddcllem  33876  sltres  33910  nolesgn2o  33919  nogesgn1o  33921  nodense  33940  nosupbnd1lem3  33958  nosupbnd1lem5  33960  nosupbnd2lem1  33963  noinfres  33970  noinfbnd1lem3  33973  noinfbnd1lem5  33975  noinfbnd2lem1  33978  noetalem1  33989  nocvxmin  34018  noeta2  34024  seglerflx  34459  seglemin  34460  btwnsegle  34464  hilbert1.1  34501  neibastop2lem  34594  bj-finsumval0  35500  relowlssretop  35578  wl-2sb6d  35757  tan2h  35813  poimirlem1  35822  poimirlem3  35824  poimirlem4  35825  poimirlem9  35830  poimirlem22  35843  poimirlem28  35849  heicant  35856  mblfinlem2  35859  itg2addnc  35875  ftc2nc  35903  dvasin  35905  sdclem1  35945  fdc  35947  istotbnd3  35973  sstotbnd  35977  prdstotbnd  35996  prdsbnd2  35997  cntotbnd  35998  rngoisocnv  36183  lsmsat  37064  islfld  37118  ps-2  37534  lplnexllnN  37620  4atlem9  37659  4atlem10a  37660  lnatexN  37835  2lnat  37840  pmapjat1  37909  lhpj1  38078  lhpm0atN  38085  4atexlemex2  38127  4atex  38132  4atex2-0aOLDN  38134  4atex2-0cOLDN  38136  lautcnvle  38145  lautj  38149  lautm  38150  idltrn  38206  cdleme01N  38277  cdleme0ex1N  38279  cdleme5  38296  cdleme9  38309  cdleme11c  38317  cdleme11g  38321  cdlemefrs29bpre0  38452  cdlemefrs29cpre1  38454  cdlemefrs32fva1  38457  cdleme32fva  38493  cdleme32fva1  38494  cdleme32fvaw  38495  cdleme32d  38500  cdleme32f  38502  cdleme35fnpq  38505  cdleme48d  38591  cdleme48gfv  38593  cdleme50ltrn  38613  trlord  38625  cdlemg4b1  38665  cdlemg4b2  38666  cdlemg13a  38707  cdlemg17a  38717  cdlemg17f  38722  erng1lem  39043  erngdvlem3  39046  erngdvlem4  39047  erng1r  39051  erngdvlem3-rN  39054  erngdvlem4-rN  39055  dva0g  39083  dialss  39102  dia0  39108  dia1N  39109  diaglbN  39111  diameetN  39112  diainN  39113  diaintclN  39114  dia1dim  39117  dia2dimlem5  39124  dia2dimlem7  39126  dia2dimlem9  39128  dia2dimlem10  39129  dia2dimlem12  39131  dia2dimlem13  39132  dvhopvadd  39149  dvhvaddass  39153  dvhopvsca  39158  tendolinv  39161  tendorinv  39162  dvhlveclem  39164  dvh0g  39167  dvheveccl  39168  dvhopN  39172  docaclN  39180  diaocN  39181  djajN  39193  dib0  39220  dib1dim  39221  dibglbN  39222  dibintclN  39223  dib1dim2  39224  diblss  39226  diblsmopel  39227  dicvaddcl  39246  dicvscacl  39247  diclspsn  39250  cdlemn4a  39255  cdlemn11c  39265  dihjustlem  39272  dihord1  39274  dihord2a  39275  dihord2b  39276  dihord2cN  39277  dihord11b  39278  dihord11c  39280  dihord2pre  39281  dihlsscpre  39290  dih1dimb  39296  dib2dim  39299  dih2dimb  39300  dih2dimbALTN  39301  dihvalcq2  39303  dihopelvalcpre  39304  dihord6apre  39312  dihord5b  39315  dihord5apre  39318  dih0  39336  dihmeetlem1N  39346  dihglblem5apreN  39347  dihglblem3N  39351  dihmeetlem2N  39355  dihglbcpreN  39356  dihmeetlem4preN  39362  dih1dimatlem0  39384  dih1dimatlem  39385  dihatlat  39390  dihatexv  39394  dihglb2  39398  dihmeet  39399  dihintcl  39400  dihmeet2  39402  doch2val2  39420  dochocss  39422  dihoml4c  39432  dochdmj1  39446  djhlj  39457  djhljjN  39458  djhjlj  39459  dihsumssj  39464  djhexmid  39467  djhlsmcl  39470  djhcvat42  39471  dihjatcclem4  39477  dihjat1lem  39484  dihsmsprn  39486  dihjat3  39488  dvh3dim2  39504  dvh3dim3N  39505  dochkr1OLDN  39535  lclkrlem2c  39565  lclkrlem2d  39566  mapdpglem23  39750  hdmap11lem2  39898  expgcd  40371  0prjspn  40502  mzpcompact2lem  40610  diophrw  40618  rexrabdioph  40653  eldioph4b  40670  pellexlem5  40692  pellfund14  40757  acongtr  40838  fnwe2lem3  40915  gicabl  40962  hbtlem2  40987  hbtlem4  40989  hbtlem5  40991  dgraalem  41008  aaitgo  41025  ntrclsk13  41719  gneispb  41779  wessf1ornlem  42766  ltdiv23neg  42982  islptre  43209  limclner  43241  icccncfext  43477  stoweidlem1  43591  stoweidlem14  43604  stoweidlem24  43614  stoweidlem46  43636  stoweidlem57  43647  dirkercncflem2  43694  fourierdlem20  43717  fourierdlem41  43738  fourierdlem46  43742  fourierdlem48  43744  fourierdlem50  43746  fourierdlem62  43758  fourierdlem63  43759  fourierdlem64  43760  fourierdlem65  43761  fourierdlem76  43772  fourierdlem79  43775  fourierdlem103  43799  fourierdlem104  43800  etransclem47  43871  iccpartiun  44944  reupr  45032  sqrtpwpw2p  45048  fmtnoprmfac1lem  45074  fmtnoprmfac2lem1  45076  lighneallem4a  45118  requad2  45133  perfectALTV  45233  nnsum4primeseven  45310  nnsum4primesevenALTV  45311  mgmpropd  45387  lidlmmgm  45541  gsumlsscl  45777  lincsumcl  45830  lincscmcl  45831  isldepslvec2  45884  m1modmmod  45925  elbigo2  45956  relogbdivb  45966  blennnt2  45993  dignn0ldlem  46006  itsclc0yqsollem2  46167  inlinecirc02p  46191  lubeldm2  46308  glbeldm2  46309  lubsscl  46312  glbsscl  46313  isclatd  46327  fullthinc  46385