Theorem syl122anc 1376

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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

This theorem is referenced by:  divdiv32d  11479  divcan5d  11480  divcan7d  11482  divdiv1d  11485  divdiv2d  11486  seqcoll  13874  cau3lem  14762  eqsqrtd  14775  isercolllem2  15070  isercoll  15072  summolem2a  15120  divrcnv  15255  prodmolem2a  15336  prmind2  16081  divnumden  16143  pceulem  16237  pcqmul  16245  pcqdiv  16249  pcexp  16251  pcaddlem  16279  pcbc  16291  prmodvdslcmf  16438  latledi  17765  latjjdi  17779  latjjdir  17780  sylow1lem1  18790  sylow1lem5  18794  efgred2  18946  abladdsub4  19002  ablpnpcan  19008  ghmplusg  19034  frgpnabllem2  19062  isabvd  19659  lmodvs1  19730  lspsolvlem  19982  frgpcyg  20341  ip2di  20406  evlslem1  20845  mdetuni0  21321  cpmadugsumlemB  21574  elptr2  22274  blss2ps  23105  blss2  23106  blssps  23126  blss  23127  xmeter  23135  metdcnlem  23537  lebnumii  23667  minveclem2  24126  pjthlem1  24137  volfiniun  24247  dvfsumrlimge0  24729  lgsdi  26017  ax5seglem3  26824  ax5seglem6  26827  axcontlem8  26864  eengtrkg  26879  vacn  28576  minvecolem2  28757  minvecolem4  28762  disjabrex  30443  disjabrexf  30444  2ndresdju  30509  fnpreimac  30532  slmdvs1  30999  slmd0vs  31003  orngsqr  31029  ornglmulle  31030  orngrmulle  31031  orngmullt  31034  suborng  31040  isprmidlc  31144  madjusmdetlem1  31298  cgrcomand  33842  cgrcomr  33848  cgrcomland  33850  cgrcomrand  33851  cgrtriv  33853  cgrid2  33854  ofscom  33858  cgrextend  33859  segconeq  33861  btwntriv2  33863  btwnexch3and  33872  btwnouttr2  33873  btwnouttr  33875  btwnexch  33876  btwnexchand  33877  btwndiff  33878  ifscgr  33895  cgrsub  33896  cgrxfr  33906  lineext  33927  endofsegid  33936  btwnconn1lem2  33939  btwnconn1lem3  33940  btwnconn1lem4  33941  btwnconn1lem5  33942  btwnconn1lem7  33944  btwnconn1lem8  33945  btwnconn1lem10  33947  btwnconn1lem11  33948  btwnconn1lem13  33950  btwnconn1lem14  33951  btwnconn3  33954  midofsegid  33955  segcon2  33956  brsegle2  33960  seglecgr12im  33961  seglecgr12  33962  seglerflx  33963  seglemin  33964  segletr  33965  btwnsegle  33968  colinbtwnle  33969  btwnoutside  33976  broutsideof3  33977  outsideoftr  33980  outsideofeq  33981  outsidele  33983  lineunray  33998  lineelsb2  33999  lfladdcl  36647  lshpkrlem4  36689  latmmdiN  36810  latmmdir  36811  hlatj4  36950  4atlem4b  37176  4atlem11  37185  4atlem12  37188  dalem2  37237  dalem-cly  37247  dalem10  37249  dalem23  37272  dalem38  37286  dalem44  37292  dalem55  37303  cdlema1N  37367  paddclN  37418  pmapjoin  37428  dalawlem3  37449  dalawlem5  37451  dalawlem7  37453  dalawlem8  37454  dalawlem11  37457  dalawlem12  37458  lhpexle3lem  37587  4atexlemc  37645  trlnidat  37749  arglem1N  37766  cdlemd9  37782  cdleme0moN  37801  cdleme11c  37837  cdleme11h  37842  cdleme11  37846  cdleme16c  37856  cdleme16f  37859  cdlemeda  37874  cdleme20l2  37897  cdlemefs32sn1aw  37990  cdleme43fsv1snlem  37996  cdleme41sn3a  38009  cdleme32fva  38013  cdleme32b  38018  cdleme32c  38019  cdleme32e  38021  cdleme40m  38043  cdleme40n  38044  cdleme42e  38055  cdleme48d  38111  cdlemf2  38138  cdlemf  38139  cdlemg2fv2  38176  cdlemg7fvbwN  38183  cdlemg7fvN  38200  cdlemg9a  38208  cdlemg9b  38209  cdlemg10a  38216  cdlemg12b  38220  cdlemg17b  38238  cdlemg31d  38276  cdlemg33b0  38277  cdlemg33a  38282  ltrnco  38295  ltrncom  38314  cdlemh  38393  cdlemk3  38409  cdlemk12  38426  cdlemk12u  38448  cdlemkfid1N  38497  cdlemk51  38529  cdlemk54  38534  cdlemk43N  38539  cdlemk35u  38540  cdlemk55u1  38541  cdlemk39u1  38543  cdlemk19u1  38545  dia2dimlem10  38649  dvhgrp  38683  dvh0g  38687  cdlemm10N  38694  diblsmopel  38747  cdlemn4  38774  cdlemn6  38778  cdlemn7  38779  dihordlem7  38790  dihord1  38794  dihord2pre  38801  dihvalcqat  38815  dihopelvalcpre  38824  dihord5apre  38838  dihord  38840  dih1  38862  dihglbcpreN  38876  dihjatc1  38887  dihmeetlem13N  38895  dihmeetALTN  38903  dihjatcclem1  38994  baerlem3lem1  39283  pellfundex  40200  rmxypairf1o  40225  rmxycomplete  40231  rmxyneg  40234  rmxyadd  40235  rmxy1  40236  rmxy0  40237  jm2.22  40309  proot1mul  40516  deg1mhm  40524  stoweidlem7  43015  stoweidlem36  43044