Theorem syl12anc 1324

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	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca32 558	. 2 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
5		syl12anc.4	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
6	4, 5	syl 17	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  syl22anc  1327  raaan  4082  soltmin  5532  xpdifid  5562  f1dom3fv3dif  6525  f1prex  6539  cocan1  6546  fliftfun  6562  soisores  6577  soisoi  6578  isopolem  6595  f1oiso2  6602  weniso  6604  caovcld  6827  caovcomd  6830  onminex  7007  tfrlem12  7485  omeulem1  7662  oaabs2  7725  omabs  7727  erov  7844  findcard2d  8202  frfi  8205  finsschain  8273  suplub2  8367  supgtoreq  8376  supisolem  8379  ordiso2  8420  ordtypelem7  8429  wemaplem2  8452  wemapsolem  8455  cantnflt  8569  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1  8586  wemapwe  8594  cnfcomlem  8596  cnfcom  8597  cnfcom3lem  8600  infxpenlem  8836  fseqenlem1  8847  dfac12lem2  8966  infpssrlem4  9128  enfin2i  9143  isf34lem7  9201  isf34lem6  9202  fin1a2lem7  9228  fin1a2lem10  9231  fin1a2lem11  9232  fin1a2lem13  9234  ttukeylem6  9336  ttukeylem7  9337  iundom2g  9362  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem9  9460  fpwwe2lem12  9463  fpwwe2  9465  canthnumlem  9470  canthwelem  9472  canthp1lem2  9475  pwfseqlem4  9484  inar1  9597  intgru  9636  distrlem4pr  9848  conjmul  10742  lediv12a  10916  recp1lt1  10921  cju  11016  gtndiv  11454  zsupss  11777  uzsupss  11780  icc0  12223  iccssioo2  12246  fzrev3  12406  ico01fl0  12620  fldiv  12659  modabs  12703  modltm1p1mod  12722  modifeq2int  12732  seqcaopr  12838  seqf1olem1  12840  seqof2  12859  crreczi  12989  seqcoll  13248  seqcoll2  13249  hashtpg  13267  swrdccat3b  13496  sqrlem2  13984  resqrex  13991  abs1m  14075  isercoll  14398  zsum  14449  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  efsub  14830  bitsinv2  15165  sqgcd  15278  qredeu  15372  isprm7  15420  pcpremul  15548  pceulem  15550  pczpre  15552  pcdiv  15557  pcqmul  15558  pcqdiv  15562  pcexp  15564  pcdvdsb  15573  pcneg  15578  pcdvdstr  15580  pcgcd1  15581  pc2dvds  15583  pcz  15585  pcaddlem  15592  pcadd  15593  qexpz  15605  expnprm  15606  infpnlem2  15615  ramub2  15718  ramub1lem1  15730  setsstruct2  15896  f1ocpbllem  16184  f1ovscpbl  16186  mreexexlem3d  16306  mreexexlem4d  16307  fthi  16578  ipodrsima  17165  mndpropd  17316  grpsubpropd2  17521  ghmf1  17689  symgfvne  17808  f1omvdmvd  17863  f1otrspeq  17867  pmtrdifwrdel  17905  pmtrdifwrdel2  17906  psgnunilem2  17915  psgnunilem3  17916  psgnvalii  17929  odf1  17979  lsmpropd  18090  ablnnncan  18228  gsummptshft  18336  dprdf1o  18431  pgpfac1lem3  18476  pgpfac1lem5  18478  pgpfaclem1  18480  ablfaclem2  18485  srgbinomlem3  18542  ringpropd  18582  f1rhm0to0  18740  lmodprop2d  18925  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  lbsextlem3  19160  assapropd  19327  psrass1  19405  psrass23l  19408  psrass23  19410  mplsubrg  19440  mplmon  19463  mplmonmul  19464  mplcoe1  19465  mplbas2  19470  mplind  19502  evlslem2  19512  mpfind  19536  gsumply1subr  19604  psrplusgpropd  19606  ply1scln0  19661  iporthcom  19980  obslbs  20074  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  smatvscl  20330  scmatrhmcl  20334  mat1scmat  20345  smadiadetglem2  20478  cramerimplem2  20490  cramerimplem3  20491  cramerimp  20492  1pmatscmul  20507  mat2pmatf1  20534  pm2mp  20630  chmatcl  20633  chmatval  20634  chmaidscmat  20653  chfacfisf  20659  cayhamlem1  20671  cpmidgsumm2pm  20674  cpmidpmat  20678  cpmadugsumfi  20682  cpmadumatpoly  20688  cayhamlem3  20692  pptbas  20812  elcls  20877  neiint  20908  neiptopnei  20936  restbas  20962  neitr  20984  iscnp4  21067  cnconst2  21087  cnpdis  21097  cnt0  21150  cnhaus  21158  cmpcovf  21194  hauscmplem  21209  conncompid  21234  2ndci  21251  2ndc1stc  21254  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  2ndcsep  21262  dis2ndc  21263  restlly  21286  islly2  21287  lly1stc  21299  dislly  21300  finlocfin  21323  dissnlocfin  21332  locfindis  21333  llycmpkgen2  21353  ptbasfi  21384  neitx  21410  ptpjopn  21415  ptcnplem  21424  upxp  21426  txlly  21439  txtube  21443  tx1stc  21453  txkgen  21455  xkococnlem  21462  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  hmeoimaf1o  21573  reghmph  21596  nrmhmph  21597  ordthmeolem  21604  trfil2  21691  fmfnfm  21762  hauspwpwf1  21791  fclsfnflim  21831  cnextf  21870  cnextcn  21871  tmdgsum2  21900  symgtgp  21905  subgntr  21910  opnsubg  21911  ghmcnp  21918  qustgpopn  21923  tsmsf1o  21948  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  ustexsym  22019  restutop  22041  imasdsf1olem  22178  blssexps  22231  blssex  22232  ssblex  22233  imasf1oxms  22294  blcld  22310  stdbdmopn  22323  met1stc  22326  met2ndci  22327  prdsxmslem2  22334  metcnp3  22345  cfilucfil  22364  ngptgp  22440  tgioo  22599  tgqioo  22603  zdis  22619  iccpnfhmeo  22744  xrhmeo  22745  cnheibor  22754  elpi1i  22846  cmetcusp  23150  pjthlem2  23209  ivthlem2  23221  ovolicc1  23284  ovolicc2lem3  23287  ovolicc2lem4  23288  volsup  23324  volivth  23375  vitalilem3  23379  mbflimsup  23433  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem5  23486  limcnlp  23642  limcflf  23645  limciun  23658  dvmptfsum  23738  dvcnvlem  23739  dvcvx  23783  facth1  23924  elply2  23952  plypf1  23968  coeeq  23983  aaliou3lem8  24100  ulm2  24139  mtestbdd  24159  reeff1o  24201  dcubic2  24571  quart  24588  xrlimcnp  24695  amgm  24717  harmonicbnd4  24737  perfect  24956  dchrptlem1  24989  bposlem2  25010  lgsfcl2  25028  lgsdir  25057  lgsdi  25059  lgsne0  25060  2lgslem1a1  25114  dchrvmasumlem2  25187  chpdifbndlem2  25243  pntpbnd1  25275  pntpbnd2  25276  padicabv  25319  tgcgrxfr  25413  idmot  25432  legid  25482  btwnleg  25483  leg0  25487  tghilberti1  25532  mirreu3  25549  colperpex  25625  lnopp2hpgb  25655  axcgrrflx  25794  axsegconlem1  25797  axcontlem2  25845  axcontlem12  25855  eengtrkg  25865  wwlksnredwwlkn  26790  clwwlksel  26914  clwlksfclwwlk  26962  0wlkon  26981  0trlon  26985  upgr3v3e3cycl  27040  numclwwlkovf2exlem2  27212  frgrogt3nreg  27255  nvpi  27522  nmlno0lem  27648  fh1  28477  fh2  28478  eigposi  28695  nmlnop0iALT  28854  nmopun  28873  branmfn  28964  opsqrlem1  28999  opsqrlem6  29004  mdslmd1lem1  29184  csmdsymi  29193  atom1d  29212  chirredlem2  29250  cdj1i  29292  cdj3i  29300  fcnvgreu  29472  xrofsup  29533  2sqmod  29648  archirngz  29743  archiabllem2a  29748  gsummpt2d  29781  orngsqr  29804  ornglmullt  29807  orngrmullt  29808  metideq  29936  metider  29937  pstmfval  29939  lmxrge0  29998  qqhval2  30026  qqhf  30030  qqhghm  30032  qqhrhm  30033  esumpcvgval  30140  esum2dlem  30154  esum2d  30155  sigainb  30199  insiga  30200  ddemeas  30299  imambfm  30324  dya2icoseg  30339  dya2iocnrect  30343  eulerpartlemgvv  30438  probun  30481  ballotlemfc0  30554  ballotlemfcc  30555  sgnmul  30604  signstfvneq0  30649  breprexplemc  30710  erdszelem8  31180  erdszelem9  31181  erdsze2lem2  31186  cnpconn  31212  txpconn  31214  ptpconn  31215  indispconn  31216  connpconn  31217  cvxpconn  31224  cnllysconn  31227  cvmcov2  31257  cvmopnlem  31260  cvmliftmolem1  31263  cvmliftlem14  31279  cvmliftlem15  31280  cvmlift2lem13  31297  cvmlift3lem2  31302  cvmlift3lem9  31309  poseq  31750  sltres  31815  nolesgn2o  31824  nodense  31842  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  nocvxmin  31894  seglerflx  32219  seglemin  32220  btwnsegle  32224  hilbert1.1  32261  neibastop2lem  32355  bj-finsumval0  33147  relowlssretop  33211  wl-2sb6d  33341  tan2h  33401  poimirlem1  33410  poimirlem3  33412  poimirlem4  33413  poimirlem9  33418  poimirlem22  33431  poimirlem28  33437  heicant  33444  mblfinlem2  33447  itg2addnc  33464  ftc2nc  33494  dvasin  33496  sdclem1  33539  fdc  33541  istotbnd3  33570  sstotbnd  33574  prdstotbnd  33593  prdsbnd2  33594  cntotbnd  33595  rngoisocnv  33780  lsmsat  34295  islfld  34349  ps-2  34764  lplnexllnN  34850  4atlem9  34889  4atlem10a  34890  lnatexN  35065  2lnat  35070  pmapjat1  35139  lhpj1  35308  lhpm0atN  35315  4atexlemex2  35357  4atex  35362  4atex2-0aOLDN  35364  4atex2-0cOLDN  35366  lautcnvle  35375  lautj  35379  lautm  35380  idltrn  35436  cdleme01N  35508  cdleme0ex1N  35510  cdleme5  35527  cdleme9  35540  cdleme11c  35548  cdleme11g  35552  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdlemefrs32fva1  35689  cdleme32fva  35725  cdleme32fva1  35726  cdleme32fvaw  35727  cdleme32d  35732  cdleme32f  35734  cdleme35fnpq  35737  cdleme48d  35823  cdleme48gfv  35825  cdleme50ltrn  35845  trlord  35857  cdlemg4b1  35897  cdlemg4b2  35898  cdlemg13a  35939  cdlemg17a  35949  cdlemg17f  35954  erng1lem  36275  erngdvlem3  36278  erngdvlem4  36279  erng1r  36283  erngdvlem3-rN  36286  erngdvlem4-rN  36287  dva0g  36316  dialss  36335  dia0  36341  dia1N  36342  diaglbN  36344  diameetN  36345  diainN  36346  diaintclN  36347  dia1dim  36350  dia2dimlem5  36357  dia2dimlem7  36359  dia2dimlem9  36361  dia2dimlem10  36362  dia2dimlem12  36364  dia2dimlem13  36365  dvhopvadd  36382  dvhvaddass  36386  dvhopvsca  36391  tendolinv  36394  tendorinv  36395  dvhlveclem  36397  dvh0g  36400  dvheveccl  36401  dvhopN  36405  docaclN  36413  diaocN  36414  djajN  36426  dib0  36453  dib1dim  36454  dibglbN  36455  dibintclN  36456  dib1dim2  36457  diblss  36459  diblsmopel  36460  dicvaddcl  36479  dicvscacl  36480  diclspsn  36483  cdlemn4a  36488  cdlemn11c  36498  dihjustlem  36505  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord2cN  36510  dihord11b  36511  dihord11c  36513  dihord2pre  36514  dihlsscpre  36523  dih1dimb  36529  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihvalcq2  36536  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihord5apre  36551  dih0  36569  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetlem4preN  36595  dih1dimatlem0  36617  dih1dimatlem  36618  dihatlat  36623  dihatexv  36627  dihglb2  36631  dihmeet  36632  dihintcl  36633  dihmeet2  36635  doch2val2  36653  dochocss  36655  dihoml4c  36665  dochdmj1  36679  djhlj  36690  djhljjN  36691  djhjlj  36692  dihsumssj  36697  djhexmid  36700  djhlsmcl  36703  djhcvat42  36704  dihjatcclem4  36710  dihjat1lem  36717  dihsmsprn  36719  dihjat3  36721  dvh3dim2  36737  dvh3dim3N  36738  dochkr1OLDN  36768  lclkrlem2c  36798  lclkrlem2d  36799  mapdpglem23  36983  hdmap11lem2  37134  mzpcompact2lem  37314  diophrw  37322  rexrabdioph  37358  eldioph4b  37375  pellexlem5  37397  pellfund14  37462  acongtr  37545  fnwe2lem3  37622  gicabl  37669  hbtlem2  37694  hbtlem4  37696  hbtlem5  37698  dgraalem  37715  aaitgo  37732  ioounsn  37795  ntrclsk13  38369  gneispb  38429  wessf1ornlem  39371  ltdiv23neg  39617  islptre  39851  limclner  39883  icccncfext  40100  stoweidlem1  40218  stoweidlem14  40231  stoweidlem24  40241  stoweidlem46  40263  stoweidlem57  40274  dirkercncflem2  40321  fourierdlem20  40344  fourierdlem41  40365  fourierdlem46  40369  fourierdlem48  40371  fourierdlem50  40373  fourierdlem62  40385  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem76  40399  fourierdlem79  40402  fourierdlem103  40426  fourierdlem104  40427  etransclem47  40498  raaan2  41175  iccpartiun  41370  sqrtpwpw2p  41450  fmtnoprmfac1lem  41476  fmtnoprmfac2lem1  41478  lighneallem4a  41525  perfectALTV  41632  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  mgmpropd  41775  lidlmmgm  41925  gsumlsscl  42164  lincsumcl  42220  lincscmcl  42221  isldepslvec2  42274  m1modmmod  42316  elbigo2  42346  relogbdivb  42356  blennnt2  42383  dignn0ldlem  42396