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

This theorem is referenced by:  syl22anc  836  raaan  4465  raaanv  4466  raaan2  4469  soltmin  6076  xpdifid  6106  reuop  6231  f1dom3fv3dif  7197  f1prex  7212  cocan1  7219  fliftfun  7239  soisores  7254  soisoi  7255  isopolem  7272  f1oiso2  7279  weniso  7281  caovcld  7527  caovcomd  7530  onminex  7715  poseq  8045  tfrlem12  8290  omeulem1  8484  oaabs2  8550  omabs  8552  eldifsucnn  8565  erov  8674  findcard2d  9031  frfi  9153  finsschain  9224  suplub2  9318  supgtoreq  9327  supisolem  9330  ordiso2  9372  ordtypelem7  9381  wemaplem2  9404  wemapsolem  9407  cantnflt  9529  cantnfp1lem3  9537  cantnflem1b  9543  cantnflem1  9546  wemapwe  9554  cnfcomlem  9556  cnfcom  9557  cnfcom3lem  9560  infxpenlem  9870  fseqenlem1  9881  dfac12lem2  10001  infpssrlem4  10163  enfin2i  10178  isf34lem7  10236  isf34lem6  10237  fin1a2lem7  10263  fin1a2lem10  10266  fin1a2lem11  10267  fin1a2lem13  10269  ttukeylem6  10371  ttukeylem7  10372  iundom2g  10397  fpwwe2lem5  10492  fpwwe2lem6  10493  fpwwe2lem8  10495  fpwwe2lem11  10498  fpwwe2  10500  canthnumlem  10505  canthwelem  10507  canthp1lem2  10510  pwfseqlem4  10519  inar1  10632  intgru  10671  distrlem4pr  10883  conjmul  11793  lediv12a  11969  recp1lt1  11974  cju  12070  gtndiv  12498  zsupss  12778  uzsupss  12781  icc0  13228  iccssioo2  13253  fzrev3  13423  ico01fl0  13640  fldiv  13681  modabs  13725  modltm1p1mod  13744  modifeq2int  13754  modsumfzodifsn  13765  seqcaopr  13861  seqf1olem1  13863  seqof2  13882  crreczi  14044  seqcoll  14278  seqcoll2  14279  hashtpg  14299  swrdccat3b  14551  sqrlem2  15054  resqrex  15061  abs1m  15146  isercoll  15478  zsum  15529  fsum2dlem  15581  fsumcom2  15585  fprod2dlem  15789  fprodcom2  15793  efsub  15908  bitsinv2  16249  sqgcd  16367  qredeu  16460  isprm7  16510  pcpremul  16641  pceulem  16643  pczpre  16645  pcdiv  16650  pcqmul  16651  pcqdiv  16655  pcexp  16657  pcdvdsb  16667  pcneg  16672  pcdvdstr  16674  pcgcd1  16675  pc2dvds  16677  pcz  16679  pcaddlem  16686  pcadd  16687  qexpz  16699  expnprm  16700  infpnlem2  16709  ramub2  16812  ramub1lem1  16824  setsstruct2  16972  f1ocpbllem  17332  f1ovscpbl  17334  mreexexlem3d  17452  mreexexlem4d  17453  fthi  17731  ipodrsima  18356  mndpropd  18507  grpsubpropd2  18777  ghmf1  18959  symgfvne  19084  f1omvdmvd  19147  f1otrspeq  19151  pmtrdifwrdel  19189  pmtrdifwrdel2  19190  psgnunilem2  19199  psgnunilem3  19200  psgnvalii  19213  odf1  19265  lsmpropd  19378  ablnnncan  19519  gsummptshft  19632  dprdf1o  19730  pgpfac1lem3  19775  pgpfac1lem5  19777  pgpfaclem1  19779  ablfaclem2  19784  srgbinomlem3  19873  ringpropd  19916  f1ghm0to0  20082  lmodprop2d  20291  lsspropd  20385  lmhmpropd  20441  lbspropd  20467  lbsextlem3  20528  iporthcom  20946  obslbs  21043  assapropd  21182  psrass1  21280  psrass23l  21283  psrass23  21285  mplsubrg  21317  mplmon  21342  mplmonmul  21343  mplcoe1  21344  mplbas2  21349  mplind  21384  evlslem2  21395  mpfind  21423  gsumply1subr  21511  psrplusgpropd  21513  ply1scln0  21568  scmataddcl  21771  scmatsubcl  21772  scmatmulcl  21773  smatvscl  21779  scmatrhmcl  21783  mat1scmat  21794  smadiadetglem2  21927  cramerimplem2  21939  cramerimplem3  21940  cramerimp  21941  1pmatscmul  21957  mat2pmatf1  21984  pm2mp  22080  chmatcl  22083  chmatval  22084  chmaidscmat  22103  chfacfisf  22109  cayhamlem1  22121  cpmidgsumm2pm  22124  cpmidpmat  22128  cpmadugsumfi  22132  cpmadumatpoly  22138  cayhamlem3  22142  pptbas  22264  elcls  22330  neiint  22361  neiptopnei  22389  restbas  22415  neitr  22437  iscnp4  22520  cnconst2  22540  cnpdis  22550  cnt0  22603  cnhaus  22611  cmpcovf  22648  hauscmplem  22663  conncompid  22688  2ndci  22705  2ndc1stc  22708  1stcrest  22710  2ndcctbss  22712  2ndcomap  22715  2ndcsep  22716  dis2ndc  22717  restlly  22740  islly2  22741  lly1stc  22753  dislly  22754  finlocfin  22777  dissnlocfin  22786  locfindis  22787  llycmpkgen2  22807  ptbasfi  22838  neitx  22864  ptpjopn  22869  ptcnplem  22878  upxp  22880  txlly  22893  txtube  22897  tx1stc  22907  txkgen  22909  xkococnlem  22916  kqreglem1  22998  kqreglem2  22999  kqnrmlem1  23000  kqnrmlem2  23001  hmeoimaf1o  23027  reghmph  23050  nrmhmph  23051  ordthmeolem  23058  trfil2  23144  fmfnfm  23215  hauspwpwf1  23244  fclsfnflim  23284  cnextf  23323  cnextcn  23324  tmdgsum2  23353  symgtgp  23363  subgntr  23364  opnsubg  23365  ghmcnp  23372  qustgpopn  23377  tsmsf1o  23402  tsmsxplem1  23410  tsmsxplem2  23411  tsmsxp  23412  ustexsym  23473  restutop  23495  imasdsf1olem  23632  blssexps  23685  blssex  23686  ssblex  23687  imasf1oxms  23751  blcld  23767  stdbdmopn  23780  met1stc  23783  met2ndci  23784  prdsxmslem2  23791  metcnp3  23802  cfilucfil  23821  ngptgp  23898  tgioo  24065  tgqioo  24069  zdis  24085  iccpnfhmeo  24214  xrhmeo  24215  cnheibor  24224  elpi1i  24315  cmetcusp  24624  bncssbn  24644  pjthlem2  24708  ivthlem2  24722  ovolicc1  24786  ovolicc2lem3  24789  ovolicc2lem4  24790  volsup  24826  volivth  24877  vitalilem3  24880  mbflimsup  24936  mbfi1fseqlem1  24986  mbfi1fseqlem3  24988  mbfi1fseqlem5  24990  limcnlp  25148  limcflf  25151  limciun  25164  dvmptfsum  25245  dvcnvlem  25246  dvcvx  25290  facth1  25435  elply2  25463  plypf1  25479  coeeq  25494  aaliou3lem8  25611  ulm2  25650  mtestbdd  25670  reeff1o  25712  logbgcd1irr  26050  dcubic2  26100  quart  26117  xrlimcnp  26224  amgm  26246  harmonicbnd4  26266  perfect  26485  dchrptlem1  26518  bposlem2  26539  lgsfcl2  26557  lgsdir  26586  lgsdi  26588  lgsne0  26589  2lgslem1a1  26643  2sqmod  26690  dchrvmasumlem2  26752  chpdifbndlem2  26808  pntpbnd1  26840  pntpbnd2  26841  padicabv  26884  sltres  26916  nolesgn2o  26925  nogesgn1o  26927  nodense  26946  nosupbnd1lem3  26964  nosupbnd1lem5  26966  nosupbnd2lem1  26969  noinfres  26976  noinfbnd1lem3  26979  noinfbnd1lem5  26981  noinfbnd2lem1  26984  noetalem1  26995  nocvxmin  27024  noeta2  27030  tgcgrxfr  27168  idmot  27187  legid  27237  btwnleg  27238  leg0  27242  tghilberti1  27287  mirreu3  27304  colperpex  27383  lnopp2hpgb  27413  axcgrrflx  27571  axsegconlem1  27574  axcontlem2  27622  axcontlem12  27632  eengtrkg  27643  wwlksnredwwlkn  28548  0wlkon  28772  0trlon  28776  upgr3v3e3cycl  28832  frgrogt3nreg  29049  nvpi  29317  nmlno0lem  29443  fh1  30268  fh2  30269  nmlnop0iALT  30645  nmopun  30664  branmfn  30755  opsqrlem1  30790  opsqrlem6  30795  mdslmd1lem1  30975  csmdsymi  30984  atom1d  31003  chirredlem2  31041  cdj1i  31083  cdj3i  31091  fcnvgreu  31297  suppovss  31304  xrofsup  31377  pwrssmgc  31565  gsummpt2d  31596  gsumhashmul  31603  odpmco  31642  cycpmco2lem6  31685  cycpmco2  31687  cyc3evpm  31704  cycpmconjslem2  31709  archirngz  31730  archiabllem2a  31735  sdrgdvcl  31780  sdrginvcl  31781  orngsqr  31803  ornglmullt  31806  orngrmullt  31807  lindssn  31870  lindfpropd  31873  ssmxidllem  31938  lindsun  32004  dimkerim  32006  fedgmullem2  32009  metideq  32141  metider  32142  pstmfval  32144  lmxrge0  32200  qqhval2  32230  qqhf  32234  qqhghm  32236  qqhrhm  32237  esumpcvgval  32344  esum2dlem  32358  esum2d  32359  sigainb  32402  insiga  32403  ddemeas  32502  imambfm  32529  dya2icoseg  32544  dya2iocnrect  32548  eulerpartlemgvv  32643  probun  32686  ballotlemfc0  32759  ballotlemfcc  32760  sgnmul  32809  breprexplemc  32912  erdszelem8  33459  erdszelem9  33460  erdsze2lem2  33465  cnpconn  33491  txpconn  33493  ptpconn  33494  indispconn  33495  connpconn  33496  cvxpconn  33503  cnllysconn  33506  cvmcov2  33536  cvmopnlem  33539  cvmliftmolem1  33542  cvmliftlem14  33558  cvmliftlem15  33559  cvmlift2lem13  33576  cvmlift3lem2  33581  cvmlift3lem9  33588  poxp2  34072  poxp3  34078  naddcllem  34110  seglerflx  34510  seglemin  34511  btwnsegle  34515  hilbert1.1  34552  neibastop2lem  34645  bj-finsumval0  35569  relowlssretop  35647  wl-2sb6d  35826  tan2h  35882  poimirlem1  35891  poimirlem3  35893  poimirlem4  35894  poimirlem9  35899  poimirlem22  35912  poimirlem28  35918  heicant  35925  mblfinlem2  35928  itg2addnc  35944  ftc2nc  35972  dvasin  35974  sdclem1  36014  fdc  36016  istotbnd3  36042  sstotbnd  36046  prdstotbnd  36065  prdsbnd2  36066  cntotbnd  36067  rngoisocnv  36252  lsmsat  37283  islfld  37337  ps-2  37754  lplnexllnN  37840  4atlem9  37879  4atlem10a  37880  lnatexN  38055  2lnat  38060  pmapjat1  38129  lhpj1  38298  lhpm0atN  38305  4atexlemex2  38347  4atex  38352  4atex2-0aOLDN  38354  4atex2-0cOLDN  38356  lautcnvle  38365  lautj  38369  lautm  38370  idltrn  38426  cdleme01N  38497  cdleme0ex1N  38499  cdleme5  38516  cdleme9  38529  cdleme11c  38537  cdleme11g  38541  cdlemefrs29bpre0  38672  cdlemefrs29cpre1  38674  cdlemefrs32fva1  38677  cdleme32fva  38713  cdleme32fva1  38714  cdleme32fvaw  38715  cdleme32d  38720  cdleme32f  38722  cdleme35fnpq  38725  cdleme48d  38811  cdleme48gfv  38813  cdleme50ltrn  38833  trlord  38845  cdlemg4b1  38885  cdlemg4b2  38886  cdlemg13a  38927  cdlemg17a  38937  cdlemg17f  38942  erng1lem  39263  erngdvlem3  39266  erngdvlem4  39267  erng1r  39271  erngdvlem3-rN  39274  erngdvlem4-rN  39275  dva0g  39303  dialss  39322  dia0  39328  dia1N  39329  diaglbN  39331  diameetN  39332  diainN  39333  diaintclN  39334  dia1dim  39337  dia2dimlem5  39344  dia2dimlem7  39346  dia2dimlem9  39348  dia2dimlem10  39349  dia2dimlem12  39351  dia2dimlem13  39352  dvhopvadd  39369  dvhvaddass  39373  dvhopvsca  39378  tendolinv  39381  tendorinv  39382  dvhlveclem  39384  dvh0g  39387  dvheveccl  39388  dvhopN  39392  docaclN  39400  diaocN  39401  djajN  39413  dib0  39440  dib1dim  39441  dibglbN  39442  dibintclN  39443  dib1dim2  39444  diblss  39446  diblsmopel  39447  dicvaddcl  39466  dicvscacl  39467  diclspsn  39470  cdlemn4a  39475  cdlemn11c  39485  dihjustlem  39492  dihord1  39494  dihord2a  39495  dihord2b  39496  dihord2cN  39497  dihord11b  39498  dihord11c  39500  dihord2pre  39501  dihlsscpre  39510  dih1dimb  39516  dib2dim  39519  dih2dimb  39520  dih2dimbALTN  39521  dihvalcq2  39523  dihopelvalcpre  39524  dihord6apre  39532  dihord5b  39535  dihord5apre  39538  dih0  39556  dihmeetlem1N  39566  dihglblem5apreN  39567  dihglblem3N  39571  dihmeetlem2N  39575  dihglbcpreN  39576  dihmeetlem4preN  39582  dih1dimatlem0  39604  dih1dimatlem  39605  dihatlat  39610  dihatexv  39614  dihglb2  39618  dihmeet  39619  dihintcl  39620  dihmeet2  39622  doch2val2  39640  dochocss  39642  dihoml4c  39652  dochdmj1  39666  djhlj  39677  djhljjN  39678  djhjlj  39679  dihsumssj  39684  djhexmid  39687  djhlsmcl  39690  djhcvat42  39691  dihjatcclem4  39697  dihjat1lem  39704  dihsmsprn  39706  dihjat3  39708  dvh3dim2  39724  dvh3dim3N  39725  dochkr1OLDN  39755  lclkrlem2c  39785  lclkrlem2d  39786  mapdpglem23  39970  hdmap11lem2  40118  expgcd  40602  0prjspn  40735  mzpcompact2lem  40843  diophrw  40851  rexrabdioph  40886  eldioph4b  40903  pellexlem5  40925  pellfund14  40990  acongtr  41071  fnwe2lem3  41148  gicabl  41195  hbtlem2  41220  hbtlem4  41222  hbtlem5  41224  dgraalem  41241  aaitgo  41258  ofoaid1  41333  ofoaid2  41334  ntrclsk13  42011  gneispb  42071  wessf1ornlem  43058  ltdiv23neg  43278  islptre  43505  limclner  43537  icccncfext  43773  stoweidlem1  43887  stoweidlem14  43900  stoweidlem24  43910  stoweidlem46  43932  stoweidlem57  43943  dirkercncflem2  43990  fourierdlem20  44013  fourierdlem41  44034  fourierdlem46  44038  fourierdlem48  44040  fourierdlem50  44042  fourierdlem62  44054  fourierdlem63  44055  fourierdlem64  44056  fourierdlem65  44057  fourierdlem76  44068  fourierdlem79  44071  fourierdlem103  44095  fourierdlem104  44096  etransclem47  44167  iccpartiun  45246  reupr  45334  sqrtpwpw2p  45350  fmtnoprmfac1lem  45376  fmtnoprmfac2lem1  45378  lighneallem4a  45420  requad2  45435  perfectALTV  45535  nnsum4primeseven  45612  nnsum4primesevenALTV  45613  mgmpropd  45689  lidlmmgm  45843  gsumlsscl  46079  lincsumcl  46132  lincscmcl  46133  isldepslvec2  46186  m1modmmod  46227  elbigo2  46258  relogbdivb  46268  blennnt2  46295  dignn0ldlem  46308  itsclc0yqsollem2  46469  inlinecirc02p  46493  lubeldm2  46610  glbeldm2  46611  lubsscl  46614  glbsscl  46615  isclatd  46629  fullthinc  46687