Theorem syl122anc 1406

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl122anc.6	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl122anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl122anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 521	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1402	1 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  divdiv32d  12044  divcan5d  12045  divcan7d  12047  divdiv1d  12050  divdiv2d  12051  seqcoll  14533  cau3lem  15446  eqsqrtd  15459  isercolllem2  15757  isercoll  15759  summolem2a  15805  divrcnv  15945  prodmolem2a  16027  prmind2  16781  divnumden  16845  pceulem  16943  pcqmul  16951  pcqdiv  16955  pcexp  16957  pcaddlem  16986  pcbc  16998  prmodvdslcmf  17145  latledi  18571  latjjdi  18585  latjjdir  18586  sylow1lem1  19731  sylow1lem5  19735  efgred2  19886  abladdsub4  19944  ablpnpcan  19952  ghmplusg  19979  frgpnabllem2  20007  isdomn4  20883  isabvd  20984  orngsqr  21038  ornglmulle  21039  orngrmulle  21040  orngmullt  21043  suborng  21048  lmodvs1  21080  lspsolvlem  21335  isprmidlc  21541  ssdifidlprm  21555  frgpcyg  21792  ip2di  21860  evlslem1  22304  mdetuni0  22849  cpmadugsumlemB  23105  elptr2  23806  blss2ps  24635  blss2  24636  blssps  24656  blss  24657  xmeter  24665  metdcnlem  25069  lebnumii  25200  minveclem2  25660  pjthlem1  25671  volfiniun  25781  dvfsumrlimge0  26264  lgsdi  27578  cofcut1d  28194  prlngeq  29322  ax5seglem3  29396  ax5seglem6  29399  axcontlem8  29436  eengtrkg  29451  vacn  31183  minvecolem2  31364  minvecolem4  31369  disjabrex  33063  disjabrexf  33064  2ndresdju  33130  fnpreimac  33151  cmn4d  33480  gsummulsubdishift1  33516  slmdvs1  33668  slmd0vs  33672  rlocaddval  33717  domnprodn0  33726  q1pdir  34021  madjusmdetlem1  34345  cgrcomand  36579  cgrcomr  36585  cgrcomland  36587  cgrcomrand  36588  cgrtriv  36590  cgrid2  36591  ofscom  36595  cgrextend  36596  segconeq  36598  btwntriv2  36600  btwnexch3and  36609  btwnouttr2  36610  btwnouttr  36612  btwnexch  36613  btwnexchand  36614  btwndiff  36615  ifscgr  36632  cgrsub  36633  cgrxfr  36643  lineext  36664  endofsegid  36673  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem5  36679  btwnconn1lem7  36681  btwnconn1lem8  36682  btwnconn1lem10  36684  btwnconn1lem11  36685  btwnconn1lem13  36687  btwnconn1lem14  36688  btwnconn3  36691  midofsegid  36692  segcon2  36693  brsegle2  36697  seglecgr12im  36698  seglecgr12  36699  seglerflx  36700  seglemin  36701  segletr  36702  btwnsegle  36705  colinbtwnle  36706  btwnoutside  36713  broutsideof3  36714  outsideoftr  36717  outsideofeq  36718  outsidele  36720  lineunray  36735  lineelsb2  36736  lfladdcl  39952  lshpkrlem4  39994  latmmdiN  40115  latmmdir  40116  hlatj4  40255  4atlem4b  40481  4atlem11  40490  4atlem12  40493  dalem2  40542  dalem-cly  40552  dalem10  40554  dalem23  40577  dalem38  40591  dalem44  40597  dalem55  40608  cdlema1N  40672  paddclN  40723  pmapjoin  40733  dalawlem3  40754  dalawlem5  40756  dalawlem7  40758  dalawlem8  40759  dalawlem11  40762  dalawlem12  40763  lhpexle3lem  40892  4atexlemc  40950  trlnidat  41054  arglem1N  41071  cdlemd9  41087  cdleme0moN  41106  cdleme11c  41142  cdleme11h  41147  cdleme11  41151  cdleme16c  41161  cdleme16f  41164  cdlemeda  41179  cdleme20l2  41202  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme41sn3a  41314  cdleme32fva  41318  cdleme32b  41323  cdleme32c  41324  cdleme32e  41326  cdleme40m  41348  cdleme40n  41349  cdleme42e  41360  cdleme48d  41416  cdlemf2  41443  cdlemf  41444  cdlemg2fv2  41481  cdlemg7fvbwN  41488  cdlemg7fvN  41505  cdlemg9a  41513  cdlemg9b  41514  cdlemg10a  41521  cdlemg12b  41525  cdlemg17b  41543  cdlemg31d  41581  cdlemg33b0  41582  cdlemg33a  41587  ltrnco  41600  ltrncom  41619  cdlemh  41698  cdlemk3  41714  cdlemk12  41731  cdlemk12u  41753  cdlemkfid1N  41802  cdlemk51  41834  cdlemk54  41839  cdlemk43N  41844  cdlemk35u  41845  cdlemk55u1  41846  cdlemk39u1  41848  cdlemk19u1  41850  dia2dimlem10  41954  dvhgrp  41988  dvh0g  41992  cdlemm10N  41999  diblsmopel  42052  cdlemn4  42079  cdlemn6  42083  cdlemn7  42084  dihordlem7  42095  dihord1  42099  dihord2pre  42106  dihvalcqat  42120  dihopelvalcpre  42129  dihord5apre  42143  dihord  42145  dih1  42167  dihglbcpreN  42181  dihjatc1  42192  dihmeetlem13N  42200  dihmeetALTN  42208  dihjatcclem1  42299  baerlem3lem1  42588  domnexpgn0cl  43413  pellfundex  43735  rmxypairf1o  43760  rmxycomplete  43766  rmxyneg  43769  rmxyadd  43770  rmxy1  43771  rmxy0  43772  jm2.22  43844  proot1mul  44043  deg1mhm  44049  stoweidlem7  46843  stoweidlem36  46872