Theorem syl12anc 837

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  839  raaan  4522  raaanv  4523  raaan2  4526  soltmin  6158  xpdifid  6189  reuop  6314  f1dom3fv3dif  7287  f1prex  7303  cocan1  7310  fliftfun  7331  soisores  7346  soisoi  7347  isopolem  7364  f1oiso2  7371  weniso  7373  caovcld  7625  caovcomd  7628  onminex  7821  poxp2  8166  poxp3  8173  poseq  8181  tfrlem12  8427  omeulem1  8618  nnaordex2  8675  oaabs2  8685  omabs  8687  eldifsucnn  8700  naddcllem  8712  erov  8852  findcard2d  9204  frfi  9318  finsschain  9396  suplub2  9498  supgtoreq  9507  supisolem  9510  ordiso2  9552  ordtypelem7  9561  wemaplem2  9584  wemapsolem  9587  cantnflt  9709  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1  9726  wemapwe  9734  cnfcomlem  9736  cnfcom  9737  cnfcom3lem  9740  infxpenlem  10050  fseqenlem1  10061  dfac12lem2  10182  infpssrlem4  10343  enfin2i  10358  isf34lem7  10416  isf34lem6  10417  fin1a2lem7  10443  fin1a2lem10  10446  fin1a2lem11  10447  fin1a2lem13  10449  ttukeylem6  10551  ttukeylem7  10552  iundom2g  10577  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  fpwwe2lem11  10678  fpwwe2  10680  canthnumlem  10685  canthwelem  10687  canthp1lem2  10690  pwfseqlem4  10699  inar1  10812  intgru  10851  distrlem4pr  11063  conjmul  11981  lediv12a  12158  recp1lt1  12163  cju  12259  gtndiv  12692  zsupss  12976  uzsupss  12979  icc0  13431  iccssioo2  13456  fzrev3  13626  ico01fl0  13855  fldiv  13896  modabs  13940  modltm1p1mod  13960  modifeq2int  13970  modsumfzodifsn  13981  seqcaopr  14076  seqf1olem1  14078  seqof2  14097  crreczi  14263  seqcoll  14499  seqcoll2  14500  hashtpg  14520  swrdccat3b  14774  01sqrexlem2  15278  resqrex  15285  abs1m  15370  isercoll  15700  zsum  15750  fsum2dlem  15802  fsumcom2  15806  fprod2dlem  16012  fprodcom2  16016  efsub  16132  bitsinv2  16476  sqgcd  16595  expgcd  16596  qredeu  16691  isprm7  16741  pcpremul  16876  pceulem  16878  pczpre  16880  pcdiv  16885  pcqmul  16886  pcqdiv  16890  pcexp  16892  pcdvdsb  16902  pcneg  16907  pcdvdstr  16909  pcgcd1  16910  pc2dvds  16912  pcz  16914  pcaddlem  16921  pcadd  16922  qexpz  16934  expnprm  16935  infpnlem2  16944  ramub2  17047  ramub1lem1  17059  setsstruct2  17207  f1ocpbllem  17570  f1ovscpbl  17572  mreexexlem3d  17690  mreexexlem4d  17691  fthi  17971  ipodrsima  18598  mgmpropd  18676  sgrppropd  18756  mndpropd  18784  grpsubpropd2  19076  f1ghm0to0  19275  ghmqusker  19317  symgfvne  19412  f1omvdmvd  19475  f1otrspeq  19479  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  psgnunilem2  19527  psgnunilem3  19528  psgnvalii  19541  odf1  19594  lsmpropd  19709  ablnnncan  19854  gsummptshft  19968  dprdf1o  20066  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfaclem1  20115  ablfaclem2  20120  rngpropd  20191  srgbinomlem3  20245  ringpropd  20301  lmodprop2d  20938  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  lbsextlem3  21179  iporthcom  21670  obslbs  21767  assapropd  21909  psrass1  22001  psrass23l  22004  psrass23  22006  mplsubrg  22042  mplmon  22070  mplmonmul  22071  mplcoe1  22072  mplbas2  22077  mplind  22111  evlslem2  22120  mpfind  22148  gsumply1subr  22250  psrplusgpropd  22252  ply1scln0  22310  evls1addd  22390  evls1muld  22391  evls1vsca  22392  asclply1subcl  22393  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  smatvscl  22545  scmatrhmcl  22549  mat1scmat  22560  smadiadetglem2  22693  cramerimplem2  22705  cramerimplem3  22706  cramerimp  22707  1pmatscmul  22723  mat2pmatf1  22750  pm2mp  22846  chmatcl  22849  chmatval  22850  chmaidscmat  22869  chfacfisf  22875  cayhamlem1  22887  cpmidgsumm2pm  22890  cpmidpmat  22894  cpmadugsumfi  22898  cpmadumatpoly  22904  cayhamlem3  22908  pptbas  23030  elcls  23096  neiint  23127  neiptopnei  23155  restbas  23181  neitr  23203  iscnp4  23286  cnconst2  23306  cnpdis  23316  cnt0  23369  cnhaus  23377  cmpcovf  23414  hauscmplem  23429  conncompid  23454  2ndci  23471  2ndc1stc  23474  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  2ndcsep  23482  dis2ndc  23483  restlly  23506  islly2  23507  lly1stc  23519  dislly  23520  finlocfin  23543  dissnlocfin  23552  locfindis  23553  llycmpkgen2  23573  ptbasfi  23604  neitx  23630  ptpjopn  23635  ptcnplem  23644  upxp  23646  txlly  23659  txtube  23663  tx1stc  23673  txkgen  23675  xkococnlem  23682  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  hmeoimaf1o  23793  reghmph  23816  nrmhmph  23817  ordthmeolem  23824  trfil2  23910  fmfnfm  23981  hauspwpwf1  24010  fclsfnflim  24050  cnextf  24089  cnextcn  24090  tmdgsum2  24119  symgtgp  24129  subgntr  24130  opnsubg  24131  ghmcnp  24138  qustgpopn  24143  tsmsf1o  24168  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  ustexsym  24239  restutop  24261  imasdsf1olem  24398  blssexps  24451  blssex  24452  ssblex  24453  imasf1oxms  24517  blcld  24533  stdbdmopn  24546  met1stc  24549  met2ndci  24550  prdsxmslem2  24557  metcnp3  24568  cfilucfil  24587  ngptgp  24664  tgioo  24831  tgqioo  24835  zdis  24851  iccpnfhmeo  24989  xrhmeo  24990  cnheibor  25000  elpi1i  25092  cmetcusp  25401  bncssbn  25421  pjthlem2  25485  ivthlem2  25500  ovolicc1  25564  ovolicc2lem3  25567  ovolicc2lem4  25568  volsup  25604  volivth  25655  vitalilem3  25658  mbflimsup  25714  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem5  25768  limcnlp  25927  limcflf  25930  limciun  25943  dvmptfsum  26027  dvcnvlem  26028  dvcvx  26073  facth1  26220  elply2  26249  plypf1  26265  coeeq  26280  aaliou3lem8  26401  ulm2  26442  mtestbdd  26462  reeff1o  26505  logbgcd1irr  26851  dcubic2  26901  quart  26918  xrlimcnp  27025  amgm  27048  harmonicbnd4  27068  perfect  27289  dchrptlem1  27322  bposlem2  27343  lgsfcl2  27361  lgsdir  27390  lgsdi  27392  lgsne0  27393  2lgslem1a1  27447  2sqmod  27494  dchrvmasumlem2  27556  chpdifbndlem2  27612  pntpbnd1  27644  pntpbnd2  27645  padicabv  27688  sltres  27721  nolesgn2o  27730  nogesgn1o  27732  nodense  27751  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  noetalem1  27800  nocvxmin  27837  noeta2  27843  readdscl  28445  tgcgrxfr  28540  idmot  28559  legid  28609  btwnleg  28610  leg0  28614  tghilberti1  28659  mirreu3  28676  colperpex  28755  lnopp2hpgb  28785  axcgrrflx  28943  axsegconlem1  28946  axcontlem2  28994  axcontlem12  29004  eengtrkg  29015  wwlksnredwwlkn  29924  0wlkon  30148  0trlon  30152  upgr3v3e3cycl  30208  frgrogt3nreg  30425  nvpi  30695  nmlno0lem  30821  fh1  31646  fh2  31647  nmlnop0iALT  32023  nmopun  32042  branmfn  32133  opsqrlem1  32168  opsqrlem6  32173  mdslmd1lem1  32353  csmdsymi  32362  atom1d  32381  chirredlem2  32419  cdj1i  32461  cdj3i  32469  copsex2dv  32625  fcnvgreu  32689  suppovss  32695  xrofsup  32777  nn0difffzod  32813  pwrssmgc  32974  chnind  32984  gsummpt2d  33034  gsumhashmul  33046  odpmco  33088  cycpmco2lem6  33133  cycpmco2  33135  cyc3evpm  33152  cycpmconjslem2  33157  archirngz  33178  archiabllem2a  33183  elrgspnlem4  33234  rloc0g  33257  rloc1r  33258  sdrgdvcl  33280  sdrginvcl  33281  orngsqr  33313  ornglmullt  33316  orngrmullt  33317  lindssn  33385  lindfpropd  33389  ssdifidllem  33463  ssmxidllem  33480  rsprprmprmidlb  33530  rprmirredb  33539  1arithufd  33555  ply1asclunit  33578  ply1dg1rt  33583  ply1dg3rt0irred  33586  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  lsssra  33617  lindsun  33652  dimkerim  33654  fedgmullem2  33657  irngss  33701  irngnzply1  33705  algextdeglem2  33723  algextdeglem4  33725  metideq  33853  metider  33854  pstmfval  33856  lmxrge0  33912  qqhval2  33944  qqhf  33948  qqhghm  33950  qqhrhm  33951  esumpcvgval  34058  esum2dlem  34072  esum2d  34073  sigainb  34116  insiga  34117  ddemeas  34216  imambfm  34243  dya2icoseg  34258  dya2iocnrect  34262  eulerpartlemgvv  34357  probun  34400  ballotlemfc0  34473  ballotlemfcc  34474  sgnmul  34523  breprexplemc  34625  erdszelem8  35182  erdszelem9  35183  erdsze2lem2  35188  cnpconn  35214  txpconn  35216  ptpconn  35217  indispconn  35218  connpconn  35219  cvxpconn  35226  cnllysconn  35229  cvmcov2  35259  cvmopnlem  35262  cvmliftmolem1  35265  cvmliftlem14  35281  cvmliftlem15  35282  cvmlift2lem13  35299  cvmlift3lem2  35304  cvmlift3lem9  35311  seglerflx  36093  seglemin  36094  btwnsegle  36098  hilbert1.1  36135  neibastop2lem  36342  weiunfrlem  36446  weiunso  36448  bj-finsumval0  37267  relowlssretop  37345  wl-2sb6d  37538  tan2h  37598  poimirlem1  37607  poimirlem3  37609  poimirlem4  37610  poimirlem9  37615  poimirlem22  37628  poimirlem28  37634  heicant  37641  mblfinlem2  37644  itg2addnc  37660  ftc2nc  37688  dvasin  37690  sdclem1  37729  fdc  37731  istotbnd3  37757  sstotbnd  37761  prdstotbnd  37780  prdsbnd2  37781  cntotbnd  37782  rngoisocnv  37967  lsmsat  38989  islfld  39043  ps-2  39460  lplnexllnN  39546  4atlem9  39585  4atlem10a  39586  lnatexN  39761  2lnat  39766  pmapjat1  39835  lhpj1  40004  lhpm0atN  40011  4atexlemex2  40053  4atex  40058  4atex2-0aOLDN  40060  4atex2-0cOLDN  40062  lautcnvle  40071  lautj  40075  lautm  40076  idltrn  40132  cdleme01N  40203  cdleme0ex1N  40205  cdleme5  40222  cdleme9  40235  cdleme11c  40243  cdleme11g  40247  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdlemefrs32fva1  40383  cdleme32fva  40419  cdleme32fva1  40420  cdleme32fvaw  40421  cdleme32d  40426  cdleme32f  40428  cdleme35fnpq  40431  cdleme48d  40517  cdleme48gfv  40519  cdleme50ltrn  40539  trlord  40551  cdlemg4b1  40591  cdlemg4b2  40592  cdlemg13a  40633  cdlemg17a  40643  cdlemg17f  40648  erng1lem  40969  erngdvlem3  40972  erngdvlem4  40973  erng1r  40977  erngdvlem3-rN  40980  erngdvlem4-rN  40981  dva0g  41009  dialss  41028  dia0  41034  dia1N  41035  diaglbN  41037  diameetN  41038  diainN  41039  diaintclN  41040  dia1dim  41043  dia2dimlem5  41050  dia2dimlem7  41052  dia2dimlem9  41054  dia2dimlem10  41055  dia2dimlem12  41057  dia2dimlem13  41058  dvhopvadd  41075  dvhvaddass  41079  dvhopvsca  41084  tendolinv  41087  tendorinv  41088  dvhlveclem  41090  dvh0g  41093  dvheveccl  41094  dvhopN  41098  docaclN  41106  diaocN  41107  djajN  41119  dib0  41146  dib1dim  41147  dibglbN  41148  dibintclN  41149  dib1dim2  41150  diblss  41152  diblsmopel  41153  dicvaddcl  41172  dicvscacl  41173  diclspsn  41176  cdlemn4a  41181  cdlemn11c  41191  dihjustlem  41198  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord2cN  41203  dihord11b  41204  dihord11c  41206  dihord2pre  41207  dihlsscpre  41216  dih1dimb  41222  dib2dim  41225  dih2dimb  41226  dih2dimbALTN  41227  dihvalcq2  41229  dihopelvalcpre  41230  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dih0  41262  dihmeetlem1N  41272  dihglblem5apreN  41273  dihglblem3N  41277  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetlem4preN  41288  dih1dimatlem0  41310  dih1dimatlem  41311  dihatlat  41316  dihatexv  41320  dihglb2  41324  dihmeet  41325  dihintcl  41326  dihmeet2  41328  doch2val2  41346  dochocss  41348  dihoml4c  41358  dochdmj1  41372  djhlj  41383  djhljjN  41384  djhjlj  41385  dihsumssj  41390  djhexmid  41393  djhlsmcl  41396  djhcvat42  41397  dihjatcclem4  41403  dihjat1lem  41410  dihsmsprn  41412  dihjat3  41414  dvh3dim2  41430  dvh3dim3N  41431  dochkr1OLDN  41461  lclkrlem2c  41491  lclkrlem2d  41492  mapdpglem23  41676  hdmap11lem2  41824  0prjspn  42614  mzpcompact2lem  42738  diophrw  42746  rexrabdioph  42781  eldioph4b  42798  pellexlem5  42820  pellfund14  42885  acongtr  42966  fnwe2lem3  43040  gicabl  43087  hbtlem2  43112  hbtlem4  43114  hbtlem5  43116  dgraalem  43133  aaitgo  43150  onexlimgt  43231  onexoegt  43232  oalim2cl  43278  cantnfresb  43313  onmcl  43320  tfsconcatfv  43330  tfsconcatrn  43331  ofoaid1  43347  ofoaid2  43348  ntrclsk13  44060  gneispb  44120  wessf1ornlem  45127  ltdiv23neg  45343  islptre  45574  limclner  45606  icccncfext  45842  stoweidlem1  45956  stoweidlem14  45969  stoweidlem24  45979  stoweidlem46  46001  stoweidlem57  46012  dirkercncflem2  46059  fourierdlem20  46082  fourierdlem41  46103  fourierdlem46  46107  fourierdlem48  46109  fourierdlem50  46111  fourierdlem62  46123  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem76  46137  fourierdlem79  46140  fourierdlem103  46164  fourierdlem104  46165  etransclem47  46236  iccpartiun  47358  reupr  47446  sqrtpwpw2p  47462  fmtnoprmfac1lem  47488  fmtnoprmfac2lem1  47490  lighneallem4a  47532  requad2  47547  perfectALTV  47647  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  isuspgrim0lem  47808  isuspgrim0  47809  isuspgrimlem  47811  uhgrimisgrgriclem  47835  uhgrimisgrgric  47836  clnbgrgrimlem  47838  grimgrtri  47851  gpgedgvtx1  47954  gsumlsscl  48224  lincsumcl  48276  lincscmcl  48277  isldepslvec2  48330  m1modmmod  48370  elbigo2  48401  relogbdivb  48411  blennnt2  48438  dignn0ldlem  48451  itsclc0yqsollem2  48612  inlinecirc02p  48636  lubeldm2  48752  glbeldm2  48753  lubsscl  48756  glbsscl  48757  isclatd  48771  fullthinc  48845