Theorem syl122anc 1381

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  divdiv32d  11932  divcan5d  11933  divcan7d  11935  divdiv1d  11938  divdiv2d  11939  seqcoll  14381  cau3lem  15272  eqsqrtd  15285  isercolllem2  15583  isercoll  15585  summolem2a  15632  divrcnv  15769  prodmolem2a  15851  prmind2  16606  divnumden  16669  pceulem  16767  pcqmul  16775  pcqdiv  16779  pcexp  16781  pcaddlem  16810  pcbc  16822  prmodvdslcmf  16969  latledi  18393  latjjdi  18407  latjjdir  18408  sylow1lem1  19520  sylow1lem5  19524  efgred2  19675  abladdsub4  19733  ablpnpcan  19741  ghmplusg  19768  frgpnabllem2  19796  isdomn4  20641  isabvd  20737  orngsqr  20791  ornglmulle  20792  orngrmulle  20793  orngmullt  20796  suborng  20801  lmodvs1  20833  lspsolvlem  21089  frgpcyg  21520  ip2di  21588  evlslem1  22027  mdetuni0  22546  cpmadugsumlemB  22799  elptr2  23499  blss2ps  24328  blss2  24329  blssps  24349  blss  24350  xmeter  24358  metdcnlem  24762  lebnumii  24902  minveclem2  25363  pjthlem1  25374  volfiniun  25485  dvfsumrlimge0  25974  lgsdi  27282  cofcut1d  27875  ax5seglem3  28920  ax5seglem6  28923  axcontlem8  28960  eengtrkg  28975  vacn  30685  minvecolem2  30866  minvecolem4  30871  disjabrex  32573  disjabrexf  32574  2ndresdju  32642  fnpreimac  32664  cmn4d  33024  slmdvs1  33200  slmd0vs  33204  rlocaddval  33246  domnprodn0  33253  isprmidlc  33423  ssdifidlprm  33434  q1pdir  33574  madjusmdetlem1  33851  cgrcomand  36046  cgrcomr  36052  cgrcomland  36054  cgrcomrand  36055  cgrtriv  36057  cgrid2  36058  ofscom  36062  cgrextend  36063  segconeq  36065  btwntriv2  36067  btwnexch3and  36076  btwnouttr2  36077  btwnouttr  36079  btwnexch  36080  btwnexchand  36081  btwndiff  36082  ifscgr  36099  cgrsub  36100  cgrxfr  36110  lineext  36131  endofsegid  36140  btwnconn1lem2  36143  btwnconn1lem3  36144  btwnconn1lem4  36145  btwnconn1lem5  36146  btwnconn1lem7  36148  btwnconn1lem8  36149  btwnconn1lem10  36151  btwnconn1lem11  36152  btwnconn1lem13  36154  btwnconn1lem14  36155  btwnconn3  36158  midofsegid  36159  segcon2  36160  brsegle2  36164  seglecgr12im  36165  seglecgr12  36166  seglerflx  36167  seglemin  36168  segletr  36169  btwnsegle  36172  colinbtwnle  36173  btwnoutside  36180  broutsideof3  36181  outsideoftr  36184  outsideofeq  36185  outsidele  36187  lineunray  36202  lineelsb2  36203  lfladdcl  39180  lshpkrlem4  39222  latmmdiN  39343  latmmdir  39344  hlatj4  39483  4atlem4b  39709  4atlem11  39718  4atlem12  39721  dalem2  39770  dalem-cly  39780  dalem10  39782  dalem23  39805  dalem38  39819  dalem44  39825  dalem55  39836  cdlema1N  39900  paddclN  39951  pmapjoin  39961  dalawlem3  39982  dalawlem5  39984  dalawlem7  39986  dalawlem8  39987  dalawlem11  39990  dalawlem12  39991  lhpexle3lem  40120  4atexlemc  40178  trlnidat  40282  arglem1N  40299  cdlemd9  40315  cdleme0moN  40334  cdleme11c  40370  cdleme11h  40375  cdleme11  40379  cdleme16c  40389  cdleme16f  40392  cdlemeda  40407  cdleme20l2  40430  cdlemefs32sn1aw  40523  cdleme43fsv1snlem  40529  cdleme41sn3a  40542  cdleme32fva  40546  cdleme32b  40551  cdleme32c  40552  cdleme32e  40554  cdleme40m  40576  cdleme40n  40577  cdleme42e  40588  cdleme48d  40644  cdlemf2  40671  cdlemf  40672  cdlemg2fv2  40709  cdlemg7fvbwN  40716  cdlemg7fvN  40733  cdlemg9a  40741  cdlemg9b  40742  cdlemg10a  40749  cdlemg12b  40753  cdlemg17b  40771  cdlemg31d  40809  cdlemg33b0  40810  cdlemg33a  40815  ltrnco  40828  ltrncom  40847  cdlemh  40926  cdlemk3  40942  cdlemk12  40959  cdlemk12u  40981  cdlemkfid1N  41030  cdlemk51  41062  cdlemk54  41067  cdlemk43N  41072  cdlemk35u  41073  cdlemk55u1  41074  cdlemk39u1  41076  cdlemk19u1  41078  dia2dimlem10  41182  dvhgrp  41216  dvh0g  41220  cdlemm10N  41227  diblsmopel  41280  cdlemn4  41307  cdlemn6  41311  cdlemn7  41312  dihordlem7  41323  dihord1  41327  dihord2pre  41334  dihvalcqat  41348  dihopelvalcpre  41357  dihord5apre  41371  dihord  41373  dih1  41395  dihglbcpreN  41409  dihjatc1  41420  dihmeetlem13N  41428  dihmeetALTN  41436  dihjatcclem1  41527  baerlem3lem1  41816  domnexpgn0cl  42631  pellfundex  42993  rmxypairf1o  43018  rmxycomplete  43024  rmxyneg  43027  rmxyadd  43028  rmxy1  43029  rmxy0  43030  jm2.22  43102  proot1mul  43301  deg1mhm  43307  stoweidlem7  46119  stoweidlem36  46148