Theorem syl12anc 842

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  syl22anc  844  raaan  4453  raaanv  4454  raaan2  4457  copsex2dv  5442  soltmin  6093  xpdifid  6126  reuop  6251  f1dom3fv3dif  7219  f1prex  7235  cocan1  7242  fliftfun  7263  soisores  7278  soisoi  7279  isopolem  7296  f1oiso2  7303  weniso  7305  caovcld  7556  caovcomd  7559  onminex  7752  poxp2  8090  poxp3  8097  poseq  8105  tfrlem12  8325  omeulem1  8514  nnaordex2  8572  oaabs2  8582  omabs  8584  eldifsucnn  8597  naddcllem  8609  erov  8758  findcard2d  9098  frfi  9192  finsschain  9266  suplub2  9371  supgtoreq  9381  supisolem  9384  ordiso2  9427  ordtypelem7  9436  wemaplem2  9459  wemapsolem  9462  cantnflt  9591  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1  9608  wemapwe  9616  cnfcomlem  9618  cnfcom  9619  cnfcom3lem  9622  infxpenlem  9933  fseqenlem1  9944  dfac12lem2  10065  infpssrlem4  10226  enfin2i  10241  isf34lem7  10299  isf34lem6  10300  fin1a2lem7  10326  fin1a2lem10  10329  fin1a2lem11  10330  fin1a2lem13  10332  ttukeylem6  10434  ttukeylem7  10435  iundom2g  10460  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  fpwwe2lem11  10562  fpwwe2  10564  canthnumlem  10569  canthwelem  10571  canthp1lem2  10574  pwfseqlem4  10583  inar1  10696  intgru  10735  distrlem4pr  10947  conjmul  11870  lediv12a  12047  recp1lt1  12052  cju  12153  gtndiv  12604  zsupss  12885  uzsupss  12888  icc0  13344  iccssioo2  13370  fzrev3  13542  ico01fl0  13776  fldiv  13817  modabs  13861  modltm1p1mod  13883  modifeq2int  13893  modsumfzodifsn  13904  seqcaopr  13999  seqf1olem1  14001  seqof2  14020  crreczi  14188  seqcoll  14424  seqcoll2  14425  hashtpg  14445  swrdccat3b  14700  01sqrexlem2  15203  resqrex  15210  abs1m  15296  isercoll  15628  zsum  15678  fsum2dlem  15730  fsumcom2  15734  fprod2dlem  15943  fprodcom2  15947  efsub  16065  bitsinv2  16410  sqgcd  16529  expgcd  16530  qredeu  16625  isprm7  16676  pcpremul  16812  pceulem  16814  pczpre  16816  pcdiv  16821  pcqmul  16822  pcqdiv  16826  pcexp  16828  pcdvdsb  16838  pcneg  16843  pcdvdstr  16845  pcgcd1  16846  pc2dvds  16848  pcz  16850  pcaddlem  16857  pcadd  16858  qexpz  16870  expnprm  16871  infpnlem2  16880  ramub2  16983  ramub1lem1  16995  setsstruct2  17142  f1ocpbllem  17486  f1ovscpbl  17488  mreexexlem3d  17610  mreexexlem4d  17611  fthi  17885  ipodrsima  18505  chnind  18585  mgmpropd  18617  sgrppropd  18697  mndpropd  18725  grpsubpropd2  19020  f1ghm0to0  19218  ghmqusker  19260  symgfvne  19354  f1omvdmvd  19416  f1otrspeq  19420  pmtrdifwrdel  19458  pmtrdifwrdel2  19459  psgnunilem2  19468  psgnunilem3  19469  psgnvalii  19482  odf1  19535  lsmpropd  19650  ablnnncan  19795  gsummptshft  19909  dprdf1o  20007  pgpfac1lem3  20052  pgpfac1lem5  20054  pgpfaclem1  20056  ablfaclem2  20061  rngpropd  20153  srgbinomlem3  20207  ringpropd  20267  orngsqr  20845  ornglmullt  20848  orngrmullt  20849  lmodprop2d  20921  lsspropd  21014  lmhmpropd  21070  lbspropd  21096  lbsextlem3  21160  iporthcom  21617  obslbs  21712  assapropd  21853  psrass1  21945  psrass23l  21948  psrass23  21950  mplsubrg  21986  mplmon  22018  mplmonmul  22019  mplcoe1  22020  mplbas2  22025  mplind  22053  evlslem2  22062  mpfind  22098  gsumply1subr  22225  psrplusgpropd  22227  ply1scln0  22284  evls1addd  22364  evls1muld  22365  evls1vsca  22366  asclply1subcl  22367  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  smatvscl  22514  scmatrhmcl  22518  mat1scmat  22529  smadiadetglem2  22662  cramerimplem2  22674  cramerimplem3  22675  cramerimp  22676  1pmatscmul  22692  mat2pmatf1  22719  pm2mp  22815  chmatcl  22818  chmatval  22819  chmaidscmat  22838  chfacfisf  22844  cayhamlem1  22856  cpmidgsumm2pm  22859  cpmidpmat  22863  cpmadugsumfi  22867  cpmadumatpoly  22873  cayhamlem3  22877  pptbas  22998  elcls  23063  neiint  23094  neiptopnei  23122  restbas  23148  neitr  23170  iscnp4  23253  cnconst2  23273  cnpdis  23283  cnt0  23336  cnhaus  23344  cmpcovf  23381  hauscmplem  23396  conncompid  23421  2ndci  23438  2ndc1stc  23441  1stcrest  23443  2ndcctbss  23445  2ndcomap  23448  2ndcsep  23449  dis2ndc  23450  restlly  23473  islly2  23474  lly1stc  23486  dislly  23487  finlocfin  23510  dissnlocfin  23519  locfindis  23520  llycmpkgen2  23540  ptbasfi  23571  neitx  23597  ptpjopn  23602  ptcnplem  23611  upxp  23613  txlly  23626  txtube  23630  tx1stc  23640  txkgen  23642  xkococnlem  23649  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  hmeoimaf1o  23760  reghmph  23783  nrmhmph  23784  ordthmeolem  23791  trfil2  23877  fmfnfm  23948  hauspwpwf1  23977  fclsfnflim  24017  cnextf  24056  cnextcn  24057  tmdgsum2  24086  symgtgp  24096  subgntr  24097  opnsubg  24098  ghmcnp  24105  qustgpopn  24110  tsmsf1o  24135  tsmsxplem1  24143  tsmsxplem2  24144  tsmsxp  24145  ustexsym  24206  restutop  24227  imasdsf1olem  24363  blssexps  24416  blssex  24417  ssblex  24418  imasf1oxms  24479  blcld  24495  stdbdmopn  24508  met1stc  24511  met2ndci  24512  prdsxmslem2  24519  metcnp3  24530  cfilucfil  24549  ngptgp  24626  tgioo  24786  tgqioo  24790  zdis  24807  iccpnfhmeo  24937  xrhmeo  24938  cnheibor  24947  elpi1i  25038  cmetcusp  25346  bncssbn  25366  pjthlem2  25430  ivthlem2  25444  ovolicc1  25508  ovolicc2lem3  25511  ovolicc2lem4  25512  volsup  25548  volivth  25599  vitalilem3  25602  mbflimsup  25658  mbfi1fseqlem1  25707  mbfi1fseqlem3  25709  mbfi1fseqlem5  25711  limcnlp  25870  limcflf  25873  limciun  25886  dvmptfsum  25967  dvcnvlem  25968  dvcvx  26012  facth1  26157  elply2  26186  plypf1  26202  coeeq  26217  aaliou3lem8  26336  ulm2  26375  mtestbdd  26395  reeff1o  26437  logbgcd1irr  26783  dcubic2  26833  quart  26850  xrlimcnp  26957  amgm  26979  harmonicbnd4  26999  perfect  27219  dchrptlem1  27252  bposlem2  27273  lgsfcl2  27291  lgsdir  27320  lgsdi  27322  lgsne0  27323  2lgslem1a1  27377  2sqmod  27424  dchrvmasumlem2  27486  chpdifbndlem2  27542  pntpbnd1  27574  pntpbnd2  27575  padicabv  27618  ltsres  27651  nolesgn2o  27660  nogesgn1o  27662  nodense  27681  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfres  27711  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  noetalem1  27730  nocvxmin  27772  noeta2  27778  oncutlt  28281  eucliddivs  28393  readdscl  28516  tgcgrxfr  28611  idmot  28630  legid  28680  btwnleg  28681  leg0  28685  tghilberti1  28730  mirreu3  28747  colperpex  28826  lnopp2hpgb  28856  axcgrrflx  29008  axsegconlem1  29011  axcontlem2  29059  axcontlem12  29069  eengtrkg  29080  wwlksnredwwlkn  29988  0wlkon  30215  0trlon  30219  upgr3v3e3cycl  30275  frgrogt3nreg  30492  nvpi  30763  nmlno0lem  30889  fh1  31714  fh2  31715  nmlnop0iALT  32091  nmopun  32110  branmfn  32201  opsqrlem1  32236  opsqrlem6  32241  mdslmd1lem1  32421  csmdsymi  32430  atom1d  32449  chirredlem2  32487  cdj1i  32529  cdj3i  32537  fcnvgreu  32771  suppovss  32780  xrofsup  32866  nn0difffzod  32903  sgnmul  32934  pwrssmgc  33086  gsummpt2d  33137  gsumhashmul  33155  odpmco  33174  cycpmco2lem6  33219  cycpmco2  33221  cyc3evpm  33238  cycpmconjslem2  33243  fxpsubg  33261  fxpsdrg  33263  archirngz  33277  archiabllem2a  33282  elrgspnlem4  33333  rloc0g  33359  rloc1r  33360  domnpropd  33365  sdrgdvcl  33390  sdrginvcl  33391  lindssn  33468  lindfpropd  33472  ssdifidllem  33546  ssmxidllem  33563  rsprprmprmidlb  33613  rprmirredb  33622  1arithufd  33638  ply1asclunit  33664  ply1dg1rt  33670  ply1dg3rt0irred  33674  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  psrmonmul  33741  esplyind  33766  esplyindfv  33767  lsssra  33779  lindsun  33816  dimkerim  33818  fedgmullem2  33821  fldextrspunlem1  33866  fldextrspunfld  33867  irngss  33878  irngnzply1  33882  algextdeglem2  33909  algextdeglem4  33911  constrext2chnlem  33941  metideq  34084  metider  34085  pstmfval  34087  lmxrge0  34143  qqhval2  34173  qqhf  34177  qqhghm  34179  qqhrhm  34180  esumpcvgval  34269  esum2dlem  34283  esum2d  34284  sigainb  34327  insiga  34328  ddemeas  34427  imambfm  34453  dya2icoseg  34468  dya2iocnrect  34472  eulerpartlemgvv  34567  probun  34610  ballotlemfc0  34684  ballotlemfcc  34685  breprexplemc  34823  erdszelem8  35433  erdszelem9  35434  erdsze2lem2  35439  cnpconn  35465  txpconn  35467  ptpconn  35468  indispconn  35469  connpconn  35470  cvxpconn  35477  cnllysconn  35480  cvmcov2  35510  cvmopnlem  35513  cvmliftmolem1  35516  cvmliftlem14  35532  cvmliftlem15  35533  cvmlift2lem13  35550  cvmlift3lem2  35555  cvmlift3lem9  35562  seglerflx  36347  seglemin  36348  btwnsegle  36352  hilbert1.1  36389  neibastop2lem  36595  weiunfrlem  36699  weiunso  36701  mh-inf3f1  36776  bj-finsumval0  37652  qdiff  37694  relowlssretop  37732  wl-2sb6d  37936  tan2h  37986  poimirlem1  37995  poimirlem3  37997  poimirlem4  37998  poimirlem9  38003  poimirlem22  38016  poimirlem28  38022  heicant  38029  mblfinlem2  38032  itg2addnc  38048  ftc2nc  38076  dvasin  38078  sdclem1  38117  fdc  38119  istotbnd3  38145  sstotbnd  38149  prdstotbnd  38168  prdsbnd2  38169  cntotbnd  38170  rngoisocnv  38355  lsmsat  39507  islfld  39561  ps-2  39977  lplnexllnN  40063  4atlem9  40102  4atlem10a  40103  lnatexN  40278  2lnat  40283  pmapjat1  40352  lhpj1  40521  lhpm0atN  40528  4atexlemex2  40570  4atex  40575  4atex2-0aOLDN  40577  4atex2-0cOLDN  40579  lautcnvle  40588  lautj  40592  lautm  40593  idltrn  40649  cdleme01N  40720  cdleme0ex1N  40722  cdleme5  40739  cdleme9  40752  cdleme11c  40760  cdleme11g  40764  cdlemefrs29bpre0  40895  cdlemefrs29cpre1  40897  cdlemefrs32fva1  40900  cdleme32fva  40936  cdleme32fva1  40937  cdleme32fvaw  40938  cdleme32d  40943  cdleme32f  40945  cdleme35fnpq  40948  cdleme48d  41034  cdleme48gfv  41036  cdleme50ltrn  41056  trlord  41068  cdlemg4b1  41108  cdlemg4b2  41109  cdlemg13a  41150  cdlemg17a  41160  cdlemg17f  41165  erng1lem  41486  erngdvlem3  41489  erngdvlem4  41490  erng1r  41494  erngdvlem3-rN  41497  erngdvlem4-rN  41498  dva0g  41526  dialss  41545  dia0  41551  dia1N  41552  diaglbN  41554  diameetN  41555  diainN  41556  diaintclN  41557  dia1dim  41560  dia2dimlem5  41567  dia2dimlem7  41569  dia2dimlem9  41571  dia2dimlem10  41572  dia2dimlem12  41574  dia2dimlem13  41575  dvhopvadd  41592  dvhvaddass  41596  dvhopvsca  41601  tendolinv  41604  tendorinv  41605  dvhlveclem  41607  dvh0g  41610  dvheveccl  41611  dvhopN  41615  docaclN  41623  diaocN  41624  djajN  41636  dib0  41663  dib1dim  41664  dibglbN  41665  dibintclN  41666  dib1dim2  41667  diblss  41669  diblsmopel  41670  dicvaddcl  41689  dicvscacl  41690  diclspsn  41693  cdlemn4a  41698  cdlemn11c  41708  dihjustlem  41715  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord2cN  41720  dihord11b  41721  dihord11c  41723  dihord2pre  41724  dihlsscpre  41733  dih1dimb  41739  dib2dim  41742  dih2dimb  41743  dih2dimbALTN  41744  dihvalcq2  41746  dihopelvalcpre  41747  dihord6apre  41755  dihord5b  41758  dihord5apre  41761  dih0  41779  dihmeetlem1N  41789  dihglblem5apreN  41790  dihglblem3N  41794  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetlem4preN  41805  dih1dimatlem0  41827  dih1dimatlem  41828  dihatlat  41833  dihatexv  41837  dihglb2  41841  dihmeet  41842  dihintcl  41843  dihmeet2  41845  doch2val2  41863  dochocss  41865  dihoml4c  41875  dochdmj1  41889  djhlj  41900  djhljjN  41901  djhjlj  41902  dihsumssj  41907  djhexmid  41910  djhlsmcl  41913  djhcvat42  41914  dihjatcclem4  41920  dihjat1lem  41927  dihsmsprn  41929  dihjat3  41931  dvh3dim2  41947  dvh3dim3N  41948  dochkr1OLDN  41978  lclkrlem2c  42008  lclkrlem2d  42009  mapdpglem23  42193  hdmap11lem2  42341  0prjspn  43085  mzpcompact2lem  43207  diophrw  43215  rexrabdioph  43246  eldioph4b  43263  pellexlem5  43285  pellfund14  43350  acongtr  43430  fnwe2lem3  43504  gicabl  43551  hbtlem2  43576  hbtlem4  43578  hbtlem5  43580  dgraalem  43597  aaitgo  43614  onexlimgt  43695  onexoegt  43696  oalim2cl  43741  cantnfresb  43776  onmcl  43783  tfsconcatfv  43793  tfsconcatrn  43794  ofoaid1  43810  ofoaid2  43811  ntrclsk13  44522  gneispb  44582  wessf1ornlem  45639  ltdiv23neg  45845  islptre  46071  limclner  46101  icccncfext  46337  stoweidlem1  46451  stoweidlem14  46464  stoweidlem24  46474  stoweidlem46  46496  stoweidlem57  46507  dirkercncflem2  46554  fourierdlem20  46577  fourierdlem41  46598  fourierdlem46  46602  fourierdlem48  46604  fourierdlem50  46606  fourierdlem62  46618  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem76  46632  fourierdlem79  46635  fourierdlem103  46659  fourierdlem104  46660  etransclem47  46731  m1modmmod  47834  iccpartiun  47916  reupr  48004  sqrtpwpw2p  48023  fmtnoprmfac1lem  48049  fmtnoprmfac2lem1  48051  lighneallem4a  48093  requad2  48121  perfectALTV  48221  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  isuspgrim0lem  48391  isuspgrim0  48392  isuspgrimlem  48393  upgrimwlklem2  48396  upgrimwlklem3  48397  upgrimtrlslem1  48402  uhgrimisgrgriclem  48428  uhgrimisgrgric  48429  clnbgrgrimlem  48431  grimgrtri  48447  gpgedgvtx1  48560  gpgedg2ov  48564  gpgedg2iv  48565  gsumlsscl  48878  lincsumcl  48929  lincscmcl  48930  isldepslvec2  48983  elbigo2  49050  relogbdivb  49060  blennnt2  49087  dignn0ldlem  49100  itsclc0yqsollem2  49261  inlinecirc02p  49285  lubeldm2  49453  glbeldm2  49454  lubsscl  49457  glbsscl  49458  isclatd  49480  sectpropdlem  49533  invpropdlem  49535  isopropdlem  49537  uptrlem1  49707  fucofulem1  49807  fullthinc  49947