Theorem syl12anc 834

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syl22anc  836  raaan  4460  raaanv  4461  raaan2  4464  soltmin  5996  xpdifid  6025  reuop  6144  f1dom3fv3dif  7026  f1prex  7040  cocan1  7047  fliftfun  7065  soisores  7080  soisoi  7081  isopolem  7098  f1oiso2  7105  weniso  7107  caovcld  7341  caovcomd  7344  onminex  7522  tfrlem12  8025  omeulem1  8208  oaabs2  8272  omabs  8274  erov  8394  findcard2d  8760  frfi  8763  finsschain  8831  suplub2  8925  supgtoreq  8934  supisolem  8937  ordiso2  8979  ordtypelem7  8988  wemaplem2  9011  wemapsolem  9014  cantnflt  9135  cantnfp1lem3  9143  cantnflem1b  9149  cantnflem1  9152  wemapwe  9160  cnfcomlem  9162  cnfcom  9163  cnfcom3lem  9166  infxpenlem  9439  fseqenlem1  9450  dfac12lem2  9570  infpssrlem4  9728  enfin2i  9743  isf34lem7  9801  isf34lem6  9802  fin1a2lem7  9828  fin1a2lem10  9831  fin1a2lem11  9832  fin1a2lem13  9834  ttukeylem6  9936  ttukeylem7  9937  iundom2g  9962  fpwwe2lem6  10057  fpwwe2lem7  10058  fpwwe2lem9  10060  fpwwe2lem12  10063  fpwwe2  10065  canthnumlem  10070  canthwelem  10072  canthp1lem2  10075  pwfseqlem4  10084  inar1  10197  intgru  10236  distrlem4pr  10448  conjmul  11357  lediv12a  11533  recp1lt1  11538  cju  11634  gtndiv  12060  zsupss  12338  uzsupss  12341  icc0  12787  iccssioo2  12810  fzrev3  12974  ico01fl0  13190  fldiv  13229  modabs  13273  modltm1p1mod  13292  modifeq2int  13302  modsumfzodifsn  13313  seqcaopr  13408  seqf1olem1  13410  seqof2  13429  crreczi  13590  seqcoll  13823  seqcoll2  13824  hashtpg  13844  swrdccat3b  14102  sqrlem2  14603  resqrex  14610  abs1m  14695  isercoll  15024  zsum  15075  fsum2dlem  15125  fsumcom2  15129  fprod2dlem  15334  fprodcom2  15338  efsub  15453  bitsinv2  15792  sqgcd  15909  qredeu  16002  isprm7  16052  pcpremul  16180  pceulem  16182  pczpre  16184  pcdiv  16189  pcqmul  16190  pcqdiv  16194  pcexp  16196  pcdvdsb  16205  pcneg  16210  pcdvdstr  16212  pcgcd1  16213  pc2dvds  16215  pcz  16217  pcaddlem  16224  pcadd  16225  qexpz  16237  expnprm  16238  infpnlem2  16247  ramub2  16350  ramub1lem1  16362  setsstruct2  16521  f1ocpbllem  16797  f1ovscpbl  16799  mreexexlem3d  16917  mreexexlem4d  16918  fthi  17188  ipodrsima  17775  mndpropd  17936  grpsubpropd2  18205  ghmf1  18387  symgfvne  18509  f1omvdmvd  18571  f1otrspeq  18575  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem2  18623  psgnunilem3  18624  psgnvalii  18637  odf1  18689  lsmpropd  18803  ablnnncan  18943  gsummptshft  19056  dprdf1o  19154  pgpfac1lem3  19199  pgpfac1lem5  19201  pgpfaclem1  19203  ablfaclem2  19208  srgbinomlem3  19292  ringpropd  19332  f1ghm0to0  19492  f1rhm0to0OLD  19493  lmodprop2d  19696  lsspropd  19789  lmhmpropd  19845  lbspropd  19871  lbsextlem3  19932  assapropd  20101  psrass1  20185  psrass23l  20188  psrass23  20190  mplsubrg  20220  mplmon  20244  mplmonmul  20245  mplcoe1  20246  mplbas2  20251  mplind  20282  evlslem2  20292  mpfind  20320  gsumply1subr  20402  psrplusgpropd  20404  ply1scln0  20459  iporthcom  20779  obslbs  20874  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  smatvscl  21133  scmatrhmcl  21137  mat1scmat  21148  smadiadetglem2  21281  cramerimplem2  21293  cramerimplem3  21294  cramerimp  21295  1pmatscmul  21310  mat2pmatf1  21337  pm2mp  21433  chmatcl  21436  chmatval  21437  chmaidscmat  21456  chfacfisf  21462  cayhamlem1  21474  cpmidgsumm2pm  21477  cpmidpmat  21481  cpmadugsumfi  21485  cpmadumatpoly  21491  cayhamlem3  21495  pptbas  21616  elcls  21681  neiint  21712  neiptopnei  21740  restbas  21766  neitr  21788  iscnp4  21871  cnconst2  21891  cnpdis  21901  cnt0  21954  cnhaus  21962  cmpcovf  21999  hauscmplem  22014  conncompid  22039  2ndci  22056  2ndc1stc  22059  1stcrest  22061  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  dis2ndc  22068  restlly  22091  islly2  22092  lly1stc  22104  dislly  22105  finlocfin  22128  dissnlocfin  22137  locfindis  22138  llycmpkgen2  22158  ptbasfi  22189  neitx  22215  ptpjopn  22220  ptcnplem  22229  upxp  22231  txlly  22244  txtube  22248  tx1stc  22258  txkgen  22260  xkococnlem  22267  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  hmeoimaf1o  22378  reghmph  22401  nrmhmph  22402  ordthmeolem  22409  trfil2  22495  fmfnfm  22566  hauspwpwf1  22595  fclsfnflim  22635  cnextf  22674  cnextcn  22675  tmdgsum2  22704  symgtgp  22714  subgntr  22715  opnsubg  22716  ghmcnp  22723  qustgpopn  22728  tsmsf1o  22753  tsmsxplem1  22761  tsmsxplem2  22762  tsmsxp  22763  ustexsym  22824  restutop  22846  imasdsf1olem  22983  blssexps  23036  blssex  23037  ssblex  23038  imasf1oxms  23099  blcld  23115  stdbdmopn  23128  met1stc  23131  met2ndci  23132  prdsxmslem2  23139  metcnp3  23150  cfilucfil  23169  ngptgp  23245  tgioo  23404  tgqioo  23408  zdis  23424  iccpnfhmeo  23549  xrhmeo  23550  cnheibor  23559  elpi1i  23650  cmetcusp  23957  bncssbn  23977  pjthlem2  24041  ivthlem2  24053  ovolicc1  24117  ovolicc2lem3  24120  ovolicc2lem4  24121  volsup  24157  volivth  24208  vitalilem3  24211  mbflimsup  24267  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem5  24320  limcnlp  24476  limcflf  24479  limciun  24492  dvmptfsum  24572  dvcnvlem  24573  dvcvx  24617  facth1  24758  elply2  24786  plypf1  24802  coeeq  24817  aaliou3lem8  24934  ulm2  24973  mtestbdd  24993  reeff1o  25035  logbgcd1irr  25372  dcubic2  25422  quart  25439  xrlimcnp  25546  amgm  25568  harmonicbnd4  25588  perfect  25807  dchrptlem1  25840  bposlem2  25861  lgsfcl2  25879  lgsdir  25908  lgsdi  25910  lgsne0  25911  2lgslem1a1  25965  2sqmod  26012  dchrvmasumlem2  26074  chpdifbndlem2  26130  pntpbnd1  26162  pntpbnd2  26163  padicabv  26206  tgcgrxfr  26304  idmot  26323  legid  26373  btwnleg  26374  leg0  26378  tghilberti1  26423  mirreu3  26440  colperpex  26519  lnopp2hpgb  26549  axcgrrflx  26700  axsegconlem1  26703  axcontlem2  26751  axcontlem12  26761  eengtrkg  26772  wwlksnredwwlkn  27673  0wlkon  27899  0trlon  27903  upgr3v3e3cycl  27959  frgrogt3nreg  28176  nvpi  28444  nmlno0lem  28570  fh1  29395  fh2  29396  nmlnop0iALT  29772  nmopun  29791  branmfn  29882  opsqrlem1  29917  opsqrlem6  29922  mdslmd1lem1  30102  csmdsymi  30111  atom1d  30130  chirredlem2  30168  cdj1i  30210  cdj3i  30218  fcnvgreu  30418  suppovss  30426  xrofsup  30492  gsummpt2d  30687  odpmco  30730  cycpmco2lem6  30773  cycpmco2  30775  cyc3evpm  30792  cycpmconjslem2  30797  archirngz  30818  archiabllem2a  30823  orngsqr  30877  ornglmullt  30880  orngrmullt  30881  lindssn  30939  lindfpropd  30942  ssmxidllem  30978  lindsun  31021  dimkerim  31023  fedgmullem2  31026  metideq  31133  metider  31134  pstmfval  31136  lmxrge0  31195  qqhval2  31223  qqhf  31227  qqhghm  31229  qqhrhm  31230  esumpcvgval  31337  esum2dlem  31351  esum2d  31352  sigainb  31395  insiga  31396  ddemeas  31495  imambfm  31520  dya2icoseg  31535  dya2iocnrect  31539  eulerpartlemgvv  31634  probun  31677  ballotlemfc0  31750  ballotlemfcc  31751  sgnmul  31800  breprexplemc  31903  erdszelem8  32445  erdszelem9  32446  erdsze2lem2  32451  cnpconn  32477  txpconn  32479  ptpconn  32480  indispconn  32481  connpconn  32482  cvxpconn  32489  cnllysconn  32492  cvmcov2  32522  cvmopnlem  32525  cvmliftmolem1  32528  cvmliftlem14  32544  cvmliftlem15  32545  cvmlift2lem13  32562  cvmlift3lem2  32567  cvmlift3lem9  32574  poseq  33095  sltres  33169  nolesgn2o  33178  nodense  33196  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  nocvxmin  33248  seglerflx  33573  seglemin  33574  btwnsegle  33578  hilbert1.1  33615  neibastop2lem  33708  bj-finsumval0  34570  relowlssretop  34647  wl-2sb6d  34809  tan2h  34899  poimirlem1  34908  poimirlem3  34910  poimirlem4  34911  poimirlem9  34916  poimirlem22  34929  poimirlem28  34935  heicant  34942  mblfinlem2  34945  itg2addnc  34961  ftc2nc  34991  dvasin  34993  sdclem1  35033  fdc  35035  istotbnd3  35064  sstotbnd  35068  prdstotbnd  35087  prdsbnd2  35088  cntotbnd  35089  rngoisocnv  35274  lsmsat  36159  islfld  36213  ps-2  36629  lplnexllnN  36715  4atlem9  36754  4atlem10a  36755  lnatexN  36930  2lnat  36935  pmapjat1  37004  lhpj1  37173  lhpm0atN  37180  4atexlemex2  37222  4atex  37227  4atex2-0aOLDN  37229  4atex2-0cOLDN  37231  lautcnvle  37240  lautj  37244  lautm  37245  idltrn  37301  cdleme01N  37372  cdleme0ex1N  37374  cdleme5  37391  cdleme9  37404  cdleme11c  37412  cdleme11g  37416  cdlemefrs29bpre0  37547  cdlemefrs29cpre1  37549  cdlemefrs32fva1  37552  cdleme32fva  37588  cdleme32fva1  37589  cdleme32fvaw  37590  cdleme32d  37595  cdleme32f  37597  cdleme35fnpq  37600  cdleme48d  37686  cdleme48gfv  37688  cdleme50ltrn  37708  trlord  37720  cdlemg4b1  37760  cdlemg4b2  37761  cdlemg13a  37802  cdlemg17a  37812  cdlemg17f  37817  erng1lem  38138  erngdvlem3  38141  erngdvlem4  38142  erng1r  38146  erngdvlem3-rN  38149  erngdvlem4-rN  38150  dva0g  38178  dialss  38197  dia0  38203  dia1N  38204  diaglbN  38206  diameetN  38207  diainN  38208  diaintclN  38209  dia1dim  38212  dia2dimlem5  38219  dia2dimlem7  38221  dia2dimlem9  38223  dia2dimlem10  38224  dia2dimlem12  38226  dia2dimlem13  38227  dvhopvadd  38244  dvhvaddass  38248  dvhopvsca  38253  tendolinv  38256  tendorinv  38257  dvhlveclem  38259  dvh0g  38262  dvheveccl  38263  dvhopN  38267  docaclN  38275  diaocN  38276  djajN  38288  dib0  38315  dib1dim  38316  dibglbN  38317  dibintclN  38318  dib1dim2  38319  diblss  38321  diblsmopel  38322  dicvaddcl  38341  dicvscacl  38342  diclspsn  38345  cdlemn4a  38350  cdlemn11c  38360  dihjustlem  38367  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord2cN  38372  dihord11b  38373  dihord11c  38375  dihord2pre  38376  dihlsscpre  38385  dih1dimb  38391  dib2dim  38394  dih2dimb  38395  dih2dimbALTN  38396  dihvalcq2  38398  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihord5apre  38413  dih0  38431  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetlem4preN  38457  dih1dimatlem0  38479  dih1dimatlem  38480  dihatlat  38485  dihatexv  38489  dihglb2  38493  dihmeet  38494  dihintcl  38495  dihmeet2  38497  doch2val2  38515  dochocss  38517  dihoml4c  38527  dochdmj1  38541  djhlj  38552  djhljjN  38553  djhjlj  38554  dihsumssj  38559  djhexmid  38562  djhlsmcl  38565  djhcvat42  38566  dihjatcclem4  38572  dihjat1lem  38579  dihsmsprn  38581  dihjat3  38583  dvh3dim2  38599  dvh3dim3N  38600  dochkr1OLDN  38630  lclkrlem2c  38660  lclkrlem2d  38661  mapdpglem23  38845  hdmap11lem2  38993  expgcd  39203  0prjspn  39290  mzpcompact2lem  39368  diophrw  39376  rexrabdioph  39411  eldioph4b  39428  pellexlem5  39450  pellfund14  39515  acongtr  39595  fnwe2lem3  39672  gicabl  39719  hbtlem2  39744  hbtlem4  39746  hbtlem5  39748  dgraalem  39765  aaitgo  39782  ntrclsk13  40441  gneispb  40501  wessf1ornlem  41465  ltdiv23neg  41686  islptre  41920  limclner  41952  icccncfext  42190  stoweidlem1  42306  stoweidlem14  42319  stoweidlem24  42329  stoweidlem46  42351  stoweidlem57  42362  dirkercncflem2  42409  fourierdlem20  42432  fourierdlem41  42453  fourierdlem46  42457  fourierdlem48  42459  fourierdlem50  42461  fourierdlem62  42473  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem76  42487  fourierdlem79  42490  fourierdlem103  42514  fourierdlem104  42515  etransclem47  42586  iccpartiun  43614  reupr  43704  sqrtpwpw2p  43720  fmtnoprmfac1lem  43746  fmtnoprmfac2lem1  43748  lighneallem4a  43793  requad2  43808  perfectALTV  43908  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  mgmpropd  44062  lidlmmgm  44216  gsumlsscl  44451  lincsumcl  44506  lincscmcl  44507  isldepslvec2  44560  m1modmmod  44601  elbigo2  44632  relogbdivb  44642  blennnt2  44669  dignn0ldlem  44682  itsclc0yqsollem2  44770  inlinecirc02p  44794