Theorem syl12anc 835

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl22anc  837  raaan  4418  raaanv  4419  raaan2  4422  soltmin  5963  xpdifid  5992  reuop  6112  f1dom3fv3dif  7004  f1prex  7018  cocan1  7025  fliftfun  7044  soisores  7059  soisoi  7060  isopolem  7077  f1oiso2  7084  weniso  7086  caovcld  7321  caovcomd  7324  onminex  7502  tfrlem12  8008  omeulem1  8191  oaabs2  8255  omabs  8257  erov  8377  findcard2d  8744  frfi  8747  finsschain  8815  suplub2  8909  supgtoreq  8918  supisolem  8921  ordiso2  8963  ordtypelem7  8972  wemaplem2  8995  wemapsolem  8998  cantnflt  9119  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  wemapwe  9144  cnfcomlem  9146  cnfcom  9147  cnfcom3lem  9150  infxpenlem  9424  fseqenlem1  9435  dfac12lem2  9555  infpssrlem4  9717  enfin2i  9732  isf34lem7  9790  isf34lem6  9791  fin1a2lem7  9817  fin1a2lem10  9820  fin1a2lem11  9821  fin1a2lem13  9823  ttukeylem6  9925  ttukeylem7  9926  iundom2g  9951  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  fpwwe2lem12  10052  fpwwe2  10054  canthnumlem  10059  canthwelem  10061  canthp1lem2  10064  pwfseqlem4  10073  inar1  10186  intgru  10225  distrlem4pr  10437  conjmul  11346  lediv12a  11522  recp1lt1  11527  cju  11621  gtndiv  12047  zsupss  12325  uzsupss  12328  icc0  12774  iccssioo2  12798  fzrev3  12968  ico01fl0  13184  fldiv  13223  modabs  13267  modltm1p1mod  13286  modifeq2int  13296  modsumfzodifsn  13307  seqcaopr  13403  seqf1olem1  13405  seqof2  13424  crreczi  13585  seqcoll  13818  seqcoll2  13819  hashtpg  13839  swrdccat3b  14093  sqrlem2  14595  resqrex  14602  abs1m  14687  isercoll  15016  zsum  15067  fsum2dlem  15117  fsumcom2  15121  fprod2dlem  15326  fprodcom2  15330  efsub  15445  bitsinv2  15782  sqgcd  15899  qredeu  15992  isprm7  16042  pcpremul  16170  pceulem  16172  pczpre  16174  pcdiv  16179  pcqmul  16180  pcqdiv  16184  pcexp  16186  pcdvdsb  16195  pcneg  16200  pcdvdstr  16202  pcgcd1  16203  pc2dvds  16205  pcz  16207  pcaddlem  16214  pcadd  16215  qexpz  16227  expnprm  16228  infpnlem2  16237  ramub2  16340  ramub1lem1  16352  setsstruct2  16513  f1ocpbllem  16789  f1ovscpbl  16791  mreexexlem3d  16909  mreexexlem4d  16910  fthi  17180  ipodrsima  17767  mndpropd  17928  grpsubpropd2  18197  ghmf1  18379  symgfvne  18501  f1omvdmvd  18563  f1otrspeq  18567  pmtrdifwrdel  18605  pmtrdifwrdel2  18606  psgnunilem2  18615  psgnunilem3  18616  psgnvalii  18629  odf1  18681  lsmpropd  18795  ablnnncan  18936  gsummptshft  19049  dprdf1o  19147  pgpfac1lem3  19192  pgpfac1lem5  19194  pgpfaclem1  19196  ablfaclem2  19201  srgbinomlem3  19285  ringpropd  19328  f1ghm0to0  19488  lmodprop2d  19689  lsspropd  19782  lmhmpropd  19838  lbspropd  19864  lbsextlem3  19925  iporthcom  20324  obslbs  20419  assapropd  20558  psrass1  20643  psrass23l  20646  psrass23  20648  mplsubrg  20678  mplmon  20703  mplmonmul  20704  mplcoe1  20705  mplbas2  20710  mplind  20741  evlslem2  20751  mpfind  20779  gsumply1subr  20863  psrplusgpropd  20865  ply1scln0  20920  scmataddcl  21121  scmatsubcl  21122  scmatmulcl  21123  smatvscl  21129  scmatrhmcl  21133  mat1scmat  21144  smadiadetglem2  21277  cramerimplem2  21289  cramerimplem3  21290  cramerimp  21291  1pmatscmul  21307  mat2pmatf1  21334  pm2mp  21430  chmatcl  21433  chmatval  21434  chmaidscmat  21453  chfacfisf  21459  cayhamlem1  21471  cpmidgsumm2pm  21474  cpmidpmat  21478  cpmadugsumfi  21482  cpmadumatpoly  21488  cayhamlem3  21492  pptbas  21613  elcls  21678  neiint  21709  neiptopnei  21737  restbas  21763  neitr  21785  iscnp4  21868  cnconst2  21888  cnpdis  21898  cnt0  21951  cnhaus  21959  cmpcovf  21996  hauscmplem  22011  conncompid  22036  2ndci  22053  2ndc1stc  22056  1stcrest  22058  2ndcctbss  22060  2ndcomap  22063  2ndcsep  22064  dis2ndc  22065  restlly  22088  islly2  22089  lly1stc  22101  dislly  22102  finlocfin  22125  dissnlocfin  22134  locfindis  22135  llycmpkgen2  22155  ptbasfi  22186  neitx  22212  ptpjopn  22217  ptcnplem  22226  upxp  22228  txlly  22241  txtube  22245  tx1stc  22255  txkgen  22257  xkococnlem  22264  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  hmeoimaf1o  22375  reghmph  22398  nrmhmph  22399  ordthmeolem  22406  trfil2  22492  fmfnfm  22563  hauspwpwf1  22592  fclsfnflim  22632  cnextf  22671  cnextcn  22672  tmdgsum2  22701  symgtgp  22711  subgntr  22712  opnsubg  22713  ghmcnp  22720  qustgpopn  22725  tsmsf1o  22750  tsmsxplem1  22758  tsmsxplem2  22759  tsmsxp  22760  ustexsym  22821  restutop  22843  imasdsf1olem  22980  blssexps  23033  blssex  23034  ssblex  23035  imasf1oxms  23096  blcld  23112  stdbdmopn  23125  met1stc  23128  met2ndci  23129  prdsxmslem2  23136  metcnp3  23147  cfilucfil  23166  ngptgp  23242  tgioo  23401  tgqioo  23405  zdis  23421  iccpnfhmeo  23550  xrhmeo  23551  cnheibor  23560  elpi1i  23651  cmetcusp  23958  bncssbn  23978  pjthlem2  24042  ivthlem2  24056  ovolicc1  24120  ovolicc2lem3  24123  ovolicc2lem4  24124  volsup  24160  volivth  24211  vitalilem3  24214  mbflimsup  24270  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem5  24323  limcnlp  24481  limcflf  24484  limciun  24497  dvmptfsum  24578  dvcnvlem  24579  dvcvx  24623  facth1  24765  elply2  24793  plypf1  24809  coeeq  24824  aaliou3lem8  24941  ulm2  24980  mtestbdd  25000  reeff1o  25042  logbgcd1irr  25380  dcubic2  25430  quart  25447  xrlimcnp  25554  amgm  25576  harmonicbnd4  25596  perfect  25815  dchrptlem1  25848  bposlem2  25869  lgsfcl2  25887  lgsdir  25916  lgsdi  25918  lgsne0  25919  2lgslem1a1  25973  2sqmod  26020  dchrvmasumlem2  26082  chpdifbndlem2  26138  pntpbnd1  26170  pntpbnd2  26171  padicabv  26214  tgcgrxfr  26312  idmot  26331  legid  26381  btwnleg  26382  leg0  26386  tghilberti1  26431  mirreu3  26448  colperpex  26527  lnopp2hpgb  26557  axcgrrflx  26708  axsegconlem1  26711  axcontlem2  26759  axcontlem12  26769  eengtrkg  26780  wwlksnredwwlkn  27681  0wlkon  27905  0trlon  27909  upgr3v3e3cycl  27965  frgrogt3nreg  28182  nvpi  28450  nmlno0lem  28576  fh1  29401  fh2  29402  nmlnop0iALT  29778  nmopun  29797  branmfn  29888  opsqrlem1  29923  opsqrlem6  29928  mdslmd1lem1  30108  csmdsymi  30117  atom1d  30136  chirredlem2  30174  cdj1i  30216  cdj3i  30224  fcnvgreu  30436  suppovss  30443  xrofsup  30518  pwrssmgc  30706  gsummpt2d  30734  gsumhashmul  30741  odpmco  30780  cycpmco2lem6  30823  cycpmco2  30825  cyc3evpm  30842  cycpmconjslem2  30847  archirngz  30868  archiabllem2a  30873  orngsqr  30928  ornglmullt  30931  orngrmullt  30932  lindssn  30993  lindfpropd  30996  ssmxidllem  31049  lindsun  31109  dimkerim  31111  fedgmullem2  31114  metideq  31246  metider  31247  pstmfval  31249  lmxrge0  31305  qqhval2  31333  qqhf  31337  qqhghm  31339  qqhrhm  31340  esumpcvgval  31447  esum2dlem  31461  esum2d  31462  sigainb  31505  insiga  31506  ddemeas  31605  imambfm  31630  dya2icoseg  31645  dya2iocnrect  31649  eulerpartlemgvv  31744  probun  31787  ballotlemfc0  31860  ballotlemfcc  31861  sgnmul  31910  breprexplemc  32013  erdszelem8  32558  erdszelem9  32559  erdsze2lem2  32564  cnpconn  32590  txpconn  32592  ptpconn  32593  indispconn  32594  connpconn  32595  cvxpconn  32602  cnllysconn  32605  cvmcov2  32635  cvmopnlem  32638  cvmliftmolem1  32641  cvmliftlem14  32657  cvmliftlem15  32658  cvmlift2lem13  32675  cvmlift3lem2  32680  cvmlift3lem9  32687  poseq  33208  sltres  33282  nolesgn2o  33291  nodense  33309  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd2lem1  33328  nocvxmin  33361  seglerflx  33686  seglemin  33687  btwnsegle  33691  hilbert1.1  33728  neibastop2lem  33821  bj-finsumval0  34700  relowlssretop  34780  wl-2sb6d  34959  tan2h  35049  poimirlem1  35058  poimirlem3  35060  poimirlem4  35061  poimirlem9  35066  poimirlem22  35079  poimirlem28  35085  heicant  35092  mblfinlem2  35095  itg2addnc  35111  ftc2nc  35139  dvasin  35141  sdclem1  35181  fdc  35183  istotbnd3  35209  sstotbnd  35213  prdstotbnd  35232  prdsbnd2  35233  cntotbnd  35234  rngoisocnv  35419  lsmsat  36304  islfld  36358  ps-2  36774  lplnexllnN  36860  4atlem9  36899  4atlem10a  36900  lnatexN  37075  2lnat  37080  pmapjat1  37149  lhpj1  37318  lhpm0atN  37325  4atexlemex2  37367  4atex  37372  4atex2-0aOLDN  37374  4atex2-0cOLDN  37376  lautcnvle  37385  lautj  37389  lautm  37390  idltrn  37446  cdleme01N  37517  cdleme0ex1N  37519  cdleme5  37536  cdleme9  37549  cdleme11c  37557  cdleme11g  37561  cdlemefrs29bpre0  37692  cdlemefrs29cpre1  37694  cdlemefrs32fva1  37697  cdleme32fva  37733  cdleme32fva1  37734  cdleme32fvaw  37735  cdleme32d  37740  cdleme32f  37742  cdleme35fnpq  37745  cdleme48d  37831  cdleme48gfv  37833  cdleme50ltrn  37853  trlord  37865  cdlemg4b1  37905  cdlemg4b2  37906  cdlemg13a  37947  cdlemg17a  37957  cdlemg17f  37962  erng1lem  38283  erngdvlem3  38286  erngdvlem4  38287  erng1r  38291  erngdvlem3-rN  38294  erngdvlem4-rN  38295  dva0g  38323  dialss  38342  dia0  38348  dia1N  38349  diaglbN  38351  diameetN  38352  diainN  38353  diaintclN  38354  dia1dim  38357  dia2dimlem5  38364  dia2dimlem7  38366  dia2dimlem9  38368  dia2dimlem10  38369  dia2dimlem12  38371  dia2dimlem13  38372  dvhopvadd  38389  dvhvaddass  38393  dvhopvsca  38398  tendolinv  38401  tendorinv  38402  dvhlveclem  38404  dvh0g  38407  dvheveccl  38408  dvhopN  38412  docaclN  38420  diaocN  38421  djajN  38433  dib0  38460  dib1dim  38461  dibglbN  38462  dibintclN  38463  dib1dim2  38464  diblss  38466  diblsmopel  38467  dicvaddcl  38486  dicvscacl  38487  diclspsn  38490  cdlemn4a  38495  cdlemn11c  38505  dihjustlem  38512  dihord1  38514  dihord2a  38515  dihord2b  38516  dihord2cN  38517  dihord11b  38518  dihord11c  38520  dihord2pre  38521  dihlsscpre  38530  dih1dimb  38536  dib2dim  38539  dih2dimb  38540  dih2dimbALTN  38541  dihvalcq2  38543  dihopelvalcpre  38544  dihord6apre  38552  dihord5b  38555  dihord5apre  38558  dih0  38576  dihmeetlem1N  38586  dihglblem5apreN  38587  dihglblem3N  38591  dihmeetlem2N  38595  dihglbcpreN  38596  dihmeetlem4preN  38602  dih1dimatlem0  38624  dih1dimatlem  38625  dihatlat  38630  dihatexv  38634  dihglb2  38638  dihmeet  38639  dihintcl  38640  dihmeet2  38642  doch2val2  38660  dochocss  38662  dihoml4c  38672  dochdmj1  38686  djhlj  38697  djhljjN  38698  djhjlj  38699  dihsumssj  38704  djhexmid  38707  djhlsmcl  38710  djhcvat42  38711  dihjatcclem4  38717  dihjat1lem  38724  dihsmsprn  38726  dihjat3  38728  dvh3dim2  38744  dvh3dim3N  38745  dochkr1OLDN  38775  lclkrlem2c  38805  lclkrlem2d  38806  mapdpglem23  38990  hdmap11lem2  39138  expgcd  39491  0prjspn  39614  mzpcompact2lem  39692  diophrw  39700  rexrabdioph  39735  eldioph4b  39752  pellexlem5  39774  pellfund14  39839  acongtr  39919  fnwe2lem3  39996  gicabl  40043  hbtlem2  40068  hbtlem4  40070  hbtlem5  40072  dgraalem  40089  aaitgo  40106  ntrclsk13  40774  gneispb  40834  wessf1ornlem  41811  ltdiv23neg  42030  islptre  42261  limclner  42293  icccncfext  42529  stoweidlem1  42643  stoweidlem14  42656  stoweidlem24  42666  stoweidlem46  42688  stoweidlem57  42699  dirkercncflem2  42746  fourierdlem20  42769  fourierdlem41  42790  fourierdlem46  42794  fourierdlem48  42796  fourierdlem50  42798  fourierdlem62  42810  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem76  42824  fourierdlem79  42827  fourierdlem103  42851  fourierdlem104  42852  etransclem47  42923  iccpartiun  43951  reupr  44039  sqrtpwpw2p  44055  fmtnoprmfac1lem  44081  fmtnoprmfac2lem1  44083  lighneallem4a  44126  requad2  44141  perfectALTV  44241  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  mgmpropd  44395  lidlmmgm  44549  gsumlsscl  44785  lincsumcl  44840  lincscmcl  44841  isldepslvec2  44894  m1modmmod  44935  elbigo2  44966  relogbdivb  44976  blennnt2  45003  dignn0ldlem  45016  itsclc0yqsollem2  45177  inlinecirc02p  45201