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 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	1, 4, 5	syl2anc 583	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 206  df-an 396

This theorem is referenced by:  syl22anc  835  raaan  4456  raaanv  4457  raaan2  4460  soltmin  6038  xpdifid  6068  reuop  6193  f1dom3fv3dif  7135  f1prex  7149  cocan1  7156  fliftfun  7176  soisores  7191  soisoi  7192  isopolem  7209  f1oiso2  7216  weniso  7218  caovcld  7456  caovcomd  7459  onminex  7642  tfrlem12  8204  omeulem1  8389  oaabs2  8453  omabs  8455  eldifsucnn  8468  erov  8577  findcard2d  8914  frfi  9020  finsschain  9087  suplub2  9181  supgtoreq  9190  supisolem  9193  ordiso2  9235  ordtypelem7  9244  wemaplem2  9267  wemapsolem  9270  cantnflt  9391  cantnfp1lem3  9399  cantnflem1b  9405  cantnflem1  9408  wemapwe  9416  cnfcomlem  9418  cnfcom  9419  cnfcom3lem  9422  infxpenlem  9753  fseqenlem1  9764  dfac12lem2  9884  infpssrlem4  10046  enfin2i  10061  isf34lem7  10119  isf34lem6  10120  fin1a2lem7  10146  fin1a2lem10  10149  fin1a2lem11  10150  fin1a2lem13  10152  ttukeylem6  10254  ttukeylem7  10255  iundom2g  10280  fpwwe2lem5  10375  fpwwe2lem6  10376  fpwwe2lem8  10378  fpwwe2lem11  10381  fpwwe2  10383  canthnumlem  10388  canthwelem  10390  canthp1lem2  10393  pwfseqlem4  10402  inar1  10515  intgru  10554  distrlem4pr  10766  conjmul  11675  lediv12a  11851  recp1lt1  11856  cju  11952  gtndiv  12380  zsupss  12659  uzsupss  12662  icc0  13109  iccssioo2  13134  fzrev3  13304  ico01fl0  13520  fldiv  13561  modabs  13605  modltm1p1mod  13624  modifeq2int  13634  modsumfzodifsn  13645  seqcaopr  13741  seqf1olem1  13743  seqof2  13762  crreczi  13924  seqcoll  14159  seqcoll2  14160  hashtpg  14180  swrdccat3b  14434  sqrlem2  14936  resqrex  14943  abs1m  15028  isercoll  15360  zsum  15411  fsum2dlem  15463  fsumcom2  15467  fprod2dlem  15671  fprodcom2  15675  efsub  15790  bitsinv2  16131  sqgcd  16251  qredeu  16344  isprm7  16394  pcpremul  16525  pceulem  16527  pczpre  16529  pcdiv  16534  pcqmul  16535  pcqdiv  16539  pcexp  16541  pcdvdsb  16551  pcneg  16556  pcdvdstr  16558  pcgcd1  16559  pc2dvds  16561  pcz  16563  pcaddlem  16570  pcadd  16571  qexpz  16583  expnprm  16584  infpnlem2  16593  ramub2  16696  ramub1lem1  16708  setsstruct2  16856  f1ocpbllem  17216  f1ovscpbl  17218  mreexexlem3d  17336  mreexexlem4d  17337  fthi  17615  ipodrsima  18240  mndpropd  18391  grpsubpropd2  18662  ghmf1  18844  symgfvne  18969  f1omvdmvd  19032  f1otrspeq  19036  pmtrdifwrdel  19074  pmtrdifwrdel2  19075  psgnunilem2  19084  psgnunilem3  19085  psgnvalii  19098  odf1  19150  lsmpropd  19264  ablnnncan  19405  gsummptshft  19518  dprdf1o  19616  pgpfac1lem3  19661  pgpfac1lem5  19663  pgpfaclem1  19665  ablfaclem2  19670  srgbinomlem3  19759  ringpropd  19802  f1ghm0to0  19965  lmodprop2d  20166  lsspropd  20260  lmhmpropd  20316  lbspropd  20342  lbsextlem3  20403  iporthcom  20821  obslbs  20918  assapropd  21057  psrass1  21155  psrass23l  21158  psrass23  21160  mplsubrg  21192  mplmon  21217  mplmonmul  21218  mplcoe1  21219  mplbas2  21224  mplind  21259  evlslem2  21270  mpfind  21298  gsumply1subr  21386  psrplusgpropd  21388  ply1scln0  21443  scmataddcl  21646  scmatsubcl  21647  scmatmulcl  21648  smatvscl  21654  scmatrhmcl  21658  mat1scmat  21669  smadiadetglem2  21802  cramerimplem2  21814  cramerimplem3  21815  cramerimp  21816  1pmatscmul  21832  mat2pmatf1  21859  pm2mp  21955  chmatcl  21958  chmatval  21959  chmaidscmat  21978  chfacfisf  21984  cayhamlem1  21996  cpmidgsumm2pm  21999  cpmidpmat  22003  cpmadugsumfi  22007  cpmadumatpoly  22013  cayhamlem3  22017  pptbas  22139  elcls  22205  neiint  22236  neiptopnei  22264  restbas  22290  neitr  22312  iscnp4  22395  cnconst2  22415  cnpdis  22425  cnt0  22478  cnhaus  22486  cmpcovf  22523  hauscmplem  22538  conncompid  22563  2ndci  22580  2ndc1stc  22583  1stcrest  22585  2ndcctbss  22587  2ndcomap  22590  2ndcsep  22591  dis2ndc  22592  restlly  22615  islly2  22616  lly1stc  22628  dislly  22629  finlocfin  22652  dissnlocfin  22661  locfindis  22662  llycmpkgen2  22682  ptbasfi  22713  neitx  22739  ptpjopn  22744  ptcnplem  22753  upxp  22755  txlly  22768  txtube  22772  tx1stc  22782  txkgen  22784  xkococnlem  22791  kqreglem1  22873  kqreglem2  22874  kqnrmlem1  22875  kqnrmlem2  22876  hmeoimaf1o  22902  reghmph  22925  nrmhmph  22926  ordthmeolem  22933  trfil2  23019  fmfnfm  23090  hauspwpwf1  23119  fclsfnflim  23159  cnextf  23198  cnextcn  23199  tmdgsum2  23228  symgtgp  23238  subgntr  23239  opnsubg  23240  ghmcnp  23247  qustgpopn  23252  tsmsf1o  23277  tsmsxplem1  23285  tsmsxplem2  23286  tsmsxp  23287  ustexsym  23348  restutop  23370  imasdsf1olem  23507  blssexps  23560  blssex  23561  ssblex  23562  imasf1oxms  23626  blcld  23642  stdbdmopn  23655  met1stc  23658  met2ndci  23659  prdsxmslem2  23666  metcnp3  23677  cfilucfil  23696  ngptgp  23773  tgioo  23940  tgqioo  23944  zdis  23960  iccpnfhmeo  24089  xrhmeo  24090  cnheibor  24099  elpi1i  24190  cmetcusp  24499  bncssbn  24519  pjthlem2  24583  ivthlem2  24597  ovolicc1  24661  ovolicc2lem3  24664  ovolicc2lem4  24665  volsup  24701  volivth  24752  vitalilem3  24755  mbflimsup  24811  mbfi1fseqlem1  24861  mbfi1fseqlem3  24863  mbfi1fseqlem5  24865  limcnlp  25023  limcflf  25026  limciun  25039  dvmptfsum  25120  dvcnvlem  25121  dvcvx  25165  facth1  25310  elply2  25338  plypf1  25354  coeeq  25369  aaliou3lem8  25486  ulm2  25525  mtestbdd  25545  reeff1o  25587  logbgcd1irr  25925  dcubic2  25975  quart  25992  xrlimcnp  26099  amgm  26121  harmonicbnd4  26141  perfect  26360  dchrptlem1  26393  bposlem2  26414  lgsfcl2  26432  lgsdir  26461  lgsdi  26463  lgsne0  26464  2lgslem1a1  26518  2sqmod  26565  dchrvmasumlem2  26627  chpdifbndlem2  26683  pntpbnd1  26715  pntpbnd2  26716  padicabv  26759  tgcgrxfr  26860  idmot  26879  legid  26929  btwnleg  26930  leg0  26934  tghilberti1  26979  mirreu3  26996  colperpex  27075  lnopp2hpgb  27105  axcgrrflx  27263  axsegconlem1  27266  axcontlem2  27314  axcontlem12  27324  eengtrkg  27335  wwlksnredwwlkn  28239  0wlkon  28463  0trlon  28467  upgr3v3e3cycl  28523  frgrogt3nreg  28740  nvpi  29008  nmlno0lem  29134  fh1  29959  fh2  29960  nmlnop0iALT  30336  nmopun  30355  branmfn  30446  opsqrlem1  30481  opsqrlem6  30486  mdslmd1lem1  30666  csmdsymi  30675  atom1d  30694  chirredlem2  30732  cdj1i  30774  cdj3i  30782  fcnvgreu  30989  suppovss  30996  xrofsup  31069  pwrssmgc  31257  gsummpt2d  31288  gsumhashmul  31295  odpmco  31334  cycpmco2lem6  31377  cycpmco2  31379  cyc3evpm  31396  cycpmconjslem2  31401  archirngz  31422  archiabllem2a  31427  orngsqr  31482  ornglmullt  31485  orngrmullt  31486  lindssn  31552  lindfpropd  31555  ssmxidllem  31620  lindsun  31685  dimkerim  31687  fedgmullem2  31690  metideq  31822  metider  31823  pstmfval  31825  lmxrge0  31881  qqhval2  31911  qqhf  31915  qqhghm  31917  qqhrhm  31918  esumpcvgval  32025  esum2dlem  32039  esum2d  32040  sigainb  32083  insiga  32084  ddemeas  32183  imambfm  32208  dya2icoseg  32223  dya2iocnrect  32227  eulerpartlemgvv  32322  probun  32365  ballotlemfc0  32438  ballotlemfcc  32439  sgnmul  32488  breprexplemc  32591  erdszelem8  33139  erdszelem9  33140  erdsze2lem2  33145  cnpconn  33171  txpconn  33173  ptpconn  33174  indispconn  33175  connpconn  33176  cvxpconn  33183  cnllysconn  33186  cvmcov2  33216  cvmopnlem  33219  cvmliftmolem1  33222  cvmliftlem14  33238  cvmliftlem15  33239  cvmlift2lem13  33256  cvmlift3lem2  33261  cvmlift3lem9  33268  poxp2  33769  poxp3  33775  poseq  33781  naddcllem  33810  sltres  33844  nolesgn2o  33853  nogesgn1o  33855  nodense  33874  nosupbnd1lem3  33892  nosupbnd1lem5  33894  nosupbnd2lem1  33897  noinfres  33904  noinfbnd1lem3  33907  noinfbnd1lem5  33909  noinfbnd2lem1  33912  noetalem1  33923  nocvxmin  33952  noeta2  33958  seglerflx  34393  seglemin  34394  btwnsegle  34398  hilbert1.1  34435  neibastop2lem  34528  bj-finsumval0  35435  relowlssretop  35513  wl-2sb6d  35692  tan2h  35748  poimirlem1  35757  poimirlem3  35759  poimirlem4  35760  poimirlem9  35765  poimirlem22  35778  poimirlem28  35784  heicant  35791  mblfinlem2  35794  itg2addnc  35810  ftc2nc  35838  dvasin  35840  sdclem1  35880  fdc  35882  istotbnd3  35908  sstotbnd  35912  prdstotbnd  35931  prdsbnd2  35932  cntotbnd  35933  rngoisocnv  36118  lsmsat  37001  islfld  37055  ps-2  37471  lplnexllnN  37557  4atlem9  37596  4atlem10a  37597  lnatexN  37772  2lnat  37777  pmapjat1  37846  lhpj1  38015  lhpm0atN  38022  4atexlemex2  38064  4atex  38069  4atex2-0aOLDN  38071  4atex2-0cOLDN  38073  lautcnvle  38082  lautj  38086  lautm  38087  idltrn  38143  cdleme01N  38214  cdleme0ex1N  38216  cdleme5  38233  cdleme9  38246  cdleme11c  38254  cdleme11g  38258  cdlemefrs29bpre0  38389  cdlemefrs29cpre1  38391  cdlemefrs32fva1  38394  cdleme32fva  38430  cdleme32fva1  38431  cdleme32fvaw  38432  cdleme32d  38437  cdleme32f  38439  cdleme35fnpq  38442  cdleme48d  38528  cdleme48gfv  38530  cdleme50ltrn  38550  trlord  38562  cdlemg4b1  38602  cdlemg4b2  38603  cdlemg13a  38644  cdlemg17a  38654  cdlemg17f  38659  erng1lem  38980  erngdvlem3  38983  erngdvlem4  38984  erng1r  38988  erngdvlem3-rN  38991  erngdvlem4-rN  38992  dva0g  39020  dialss  39039  dia0  39045  dia1N  39046  diaglbN  39048  diameetN  39049  diainN  39050  diaintclN  39051  dia1dim  39054  dia2dimlem5  39061  dia2dimlem7  39063  dia2dimlem9  39065  dia2dimlem10  39066  dia2dimlem12  39068  dia2dimlem13  39069  dvhopvadd  39086  dvhvaddass  39090  dvhopvsca  39095  tendolinv  39098  tendorinv  39099  dvhlveclem  39101  dvh0g  39104  dvheveccl  39105  dvhopN  39109  docaclN  39117  diaocN  39118  djajN  39130  dib0  39157  dib1dim  39158  dibglbN  39159  dibintclN  39160  dib1dim2  39161  diblss  39163  diblsmopel  39164  dicvaddcl  39183  dicvscacl  39184  diclspsn  39187  cdlemn4a  39192  cdlemn11c  39202  dihjustlem  39209  dihord1  39211  dihord2a  39212  dihord2b  39213  dihord2cN  39214  dihord11b  39215  dihord11c  39217  dihord2pre  39218  dihlsscpre  39227  dih1dimb  39233  dib2dim  39236  dih2dimb  39237  dih2dimbALTN  39238  dihvalcq2  39240  dihopelvalcpre  39241  dihord6apre  39249  dihord5b  39252  dihord5apre  39255  dih0  39273  dihmeetlem1N  39283  dihglblem5apreN  39284  dihglblem3N  39288  dihmeetlem2N  39292  dihglbcpreN  39293  dihmeetlem4preN  39299  dih1dimatlem0  39321  dih1dimatlem  39322  dihatlat  39327  dihatexv  39331  dihglb2  39335  dihmeet  39336  dihintcl  39337  dihmeet2  39339  doch2val2  39357  dochocss  39359  dihoml4c  39369  dochdmj1  39383  djhlj  39394  djhljjN  39395  djhjlj  39396  dihsumssj  39401  djhexmid  39404  djhlsmcl  39407  djhcvat42  39408  dihjatcclem4  39414  dihjat1lem  39421  dihsmsprn  39423  dihjat3  39425  dvh3dim2  39441  dvh3dim3N  39442  dochkr1OLDN  39472  lclkrlem2c  39502  lclkrlem2d  39503  mapdpglem23  39687  hdmap11lem2  39835  expgcd  40314  0prjspn  40445  mzpcompact2lem  40553  diophrw  40561  rexrabdioph  40596  eldioph4b  40613  pellexlem5  40635  pellfund14  40700  acongtr  40780  fnwe2lem3  40857  gicabl  40904  hbtlem2  40929  hbtlem4  40931  hbtlem5  40933  dgraalem  40950  aaitgo  40967  ntrclsk13  41634  gneispb  41694  wessf1ornlem  42675  ltdiv23neg  42888  islptre  43114  limclner  43146  icccncfext  43382  stoweidlem1  43496  stoweidlem14  43509  stoweidlem24  43519  stoweidlem46  43541  stoweidlem57  43552  dirkercncflem2  43599  fourierdlem20  43622  fourierdlem41  43643  fourierdlem46  43647  fourierdlem48  43649  fourierdlem50  43651  fourierdlem62  43663  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem76  43677  fourierdlem79  43680  fourierdlem103  43704  fourierdlem104  43705  etransclem47  43776  iccpartiun  44838  reupr  44926  sqrtpwpw2p  44942  fmtnoprmfac1lem  44968  fmtnoprmfac2lem1  44970  lighneallem4a  45012  requad2  45027  perfectALTV  45127  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  mgmpropd  45281  lidlmmgm  45435  gsumlsscl  45671  lincsumcl  45724  lincscmcl  45725  isldepslvec2  45778  m1modmmod  45819  elbigo2  45850  relogbdivb  45860  blennnt2  45887  dignn0ldlem  45900  itsclc0yqsollem2  46061  inlinecirc02p  46085  lubeldm2  46202  glbeldm2  46203  lubsscl  46206  glbsscl  46207  isclatd  46221  fullthinc  46279