Theorem syl122anc 1379

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 512	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1375	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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  df-3an 1089

This theorem is referenced by:  divdiv32d  12014  divcan5d  12015  divcan7d  12017  divdiv1d  12020  divdiv2d  12021  seqcoll  14424  cau3lem  15300  eqsqrtd  15313  isercolllem2  15611  isercoll  15613  summolem2a  15660  divrcnv  15797  prodmolem2a  15877  prmind2  16621  divnumden  16683  pceulem  16777  pcqmul  16785  pcqdiv  16789  pcexp  16791  pcaddlem  16820  pcbc  16832  prmodvdslcmf  16979  latledi  18429  latjjdi  18443  latjjdir  18444  sylow1lem1  19465  sylow1lem5  19469  efgred2  19620  abladdsub4  19678  ablpnpcan  19686  ghmplusg  19713  frgpnabllem2  19741  isabvd  20427  lmodvs1  20499  lspsolvlem  20754  isdomn4  20917  frgpcyg  21128  ip2di  21193  evlslem1  21644  mdetuni0  22122  cpmadugsumlemB  22375  elptr2  23077  blss2ps  23908  blss2  23909  blssps  23929  blss  23930  xmeter  23938  metdcnlem  24351  lebnumii  24481  minveclem2  24942  pjthlem1  24953  volfiniun  25063  dvfsumrlimge0  25546  lgsdi  26834  cofcut1d  27405  ax5seglem3  28186  ax5seglem6  28189  axcontlem8  28226  eengtrkg  28241  vacn  29942  minvecolem2  30123  minvecolem4  30128  disjabrex  31808  disjabrexf  31809  2ndresdju  31869  fnpreimac  31891  slmdvs1  32360  slmd0vs  32364  orngsqr  32417  ornglmulle  32418  orngrmulle  32419  orngmullt  32422  suborng  32428  isprmidlc  32561  madjusmdetlem1  32802  cgrcomand  34958  cgrcomr  34964  cgrcomland  34966  cgrcomrand  34967  cgrtriv  34969  cgrid2  34970  ofscom  34974  cgrextend  34975  segconeq  34977  btwntriv2  34979  btwnexch3and  34988  btwnouttr2  34989  btwnouttr  34991  btwnexch  34992  btwnexchand  34993  btwndiff  34994  ifscgr  35011  cgrsub  35012  cgrxfr  35022  lineext  35043  endofsegid  35052  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem7  35060  btwnconn1lem8  35061  btwnconn1lem10  35063  btwnconn1lem11  35064  btwnconn1lem13  35066  btwnconn1lem14  35067  btwnconn3  35070  midofsegid  35071  segcon2  35072  brsegle2  35076  seglecgr12im  35077  seglecgr12  35078  seglerflx  35079  seglemin  35080  segletr  35081  btwnsegle  35084  colinbtwnle  35085  btwnoutside  35092  broutsideof3  35093  outsideoftr  35096  outsideofeq  35097  outsidele  35099  lineunray  35114  lineelsb2  35115  lfladdcl  37936  lshpkrlem4  37978  latmmdiN  38099  latmmdir  38100  hlatj4  38239  4atlem4b  38466  4atlem11  38475  4atlem12  38478  dalem2  38527  dalem-cly  38537  dalem10  38539  dalem23  38562  dalem38  38576  dalem44  38582  dalem55  38593  cdlema1N  38657  paddclN  38708  pmapjoin  38718  dalawlem3  38739  dalawlem5  38741  dalawlem7  38743  dalawlem8  38744  dalawlem11  38747  dalawlem12  38748  lhpexle3lem  38877  4atexlemc  38935  trlnidat  39039  arglem1N  39056  cdlemd9  39072  cdleme0moN  39091  cdleme11c  39127  cdleme11h  39132  cdleme11  39136  cdleme16c  39146  cdleme16f  39149  cdlemeda  39164  cdleme20l2  39187  cdlemefs32sn1aw  39280  cdleme43fsv1snlem  39286  cdleme41sn3a  39299  cdleme32fva  39303  cdleme32b  39308  cdleme32c  39309  cdleme32e  39311  cdleme40m  39333  cdleme40n  39334  cdleme42e  39345  cdleme48d  39401  cdlemf2  39428  cdlemf  39429  cdlemg2fv2  39466  cdlemg7fvbwN  39473  cdlemg7fvN  39490  cdlemg9a  39498  cdlemg9b  39499  cdlemg10a  39506  cdlemg12b  39510  cdlemg17b  39528  cdlemg31d  39566  cdlemg33b0  39567  cdlemg33a  39572  ltrnco  39585  ltrncom  39604  cdlemh  39683  cdlemk3  39699  cdlemk12  39716  cdlemk12u  39738  cdlemkfid1N  39787  cdlemk51  39819  cdlemk54  39824  cdlemk43N  39829  cdlemk35u  39830  cdlemk55u1  39831  cdlemk39u1  39833  cdlemk19u1  39835  dia2dimlem10  39939  dvhgrp  39973  dvh0g  39977  cdlemm10N  39984  diblsmopel  40037  cdlemn4  40064  cdlemn6  40068  cdlemn7  40069  dihordlem7  40080  dihord1  40084  dihord2pre  40091  dihvalcqat  40105  dihopelvalcpre  40114  dihord5apre  40128  dihord  40130  dih1  40152  dihglbcpreN  40166  dihjatc1  40177  dihmeetlem13N  40185  dihmeetALTN  40193  dihjatcclem1  40284  baerlem3lem1  40573  pellfundex  41614  rmxypairf1o  41640  rmxycomplete  41646  rmxyneg  41649  rmxyadd  41650  rmxy1  41651  rmxy0  41652  jm2.22  41724  proot1mul  41931  deg1mhm  41939  stoweidlem7  44713  stoweidlem36  44742