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  12034  divcan5d  12035  divcan7d  12037  divdiv1d  12040  divdiv2d  12041  seqcoll  14521  cau3lem  15432  eqsqrtd  15445  isercolllem2  15743  isercoll  15745  summolem2a  15792  divrcnv  15932  prodmolem2a  16014  prmind2  16768  divnumden  16832  pceulem  16930  pcqmul  16938  pcqdiv  16942  pcexp  16944  pcaddlem  16973  pcbc  16985  prmodvdslcmf  17132  latledi  18558  latjjdi  18572  latjjdir  18573  sylow1lem1  19699  sylow1lem5  19703  efgred2  19854  abladdsub4  19912  ablpnpcan  19920  ghmplusg  19947  frgpnabllem2  19975  isdomn4  20851  isabvd  20952  orngsqr  21006  ornglmulle  21007  orngrmulle  21008  orngmullt  21011  suborng  21016  lmodvs1  21048  lspsolvlem  21303  isprmidlc  21509  ssdifidlprm  21523  frgpcyg  21760  ip2di  21828  evlslem1  22270  mdetuni0  22815  cpmadugsumlemB  23068  elptr2  23768  blss2ps  24597  blss2  24598  blssps  24618  blss  24619  xmeter  24627  metdcnlem  25031  lebnumii  25162  minveclem2  25622  pjthlem1  25633  volfiniun  25743  dvfsumrlimge0  26226  lgsdi  27535  cofcut1d  28151  prlngeq  29244  ax5seglem3  29318  ax5seglem6  29321  axcontlem8  29358  eengtrkg  29373  vacn  31083  minvecolem2  31264  minvecolem4  31269  disjabrex  32964  disjabrexf  32965  2ndresdju  33031  fnpreimac  33052  cmn4d  33383  gsummulsubdishift1  33419  slmdvs1  33571  slmd0vs  33575  rlocaddval  33620  domnprodn0  33629  q1pdir  33924  madjusmdetlem1  34248  cgrcomand  36504  cgrcomr  36510  cgrcomland  36512  cgrcomrand  36513  cgrtriv  36515  cgrid2  36516  ofscom  36520  cgrextend  36521  segconeq  36523  btwntriv2  36525  btwnexch3and  36534  btwnouttr2  36535  btwnouttr  36537  btwnexch  36538  btwnexchand  36539  btwndiff  36540  ifscgr  36557  cgrsub  36558  cgrxfr  36568  lineext  36589  endofsegid  36598  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem5  36604  btwnconn1lem7  36606  btwnconn1lem8  36607  btwnconn1lem10  36609  btwnconn1lem11  36610  btwnconn1lem13  36612  btwnconn1lem14  36613  btwnconn3  36616  midofsegid  36617  segcon2  36618  brsegle2  36622  seglecgr12im  36623  seglecgr12  36624  seglerflx  36625  seglemin  36626  segletr  36627  btwnsegle  36630  colinbtwnle  36631  btwnoutside  36638  broutsideof3  36639  outsideoftr  36642  outsideofeq  36643  outsidele  36645  lineunray  36660  lineelsb2  36661  lfladdcl  39886  lshpkrlem4  39928  latmmdiN  40049  latmmdir  40050  hlatj4  40189  4atlem4b  40415  4atlem11  40424  4atlem12  40427  dalem2  40476  dalem-cly  40486  dalem10  40488  dalem23  40511  dalem38  40525  dalem44  40531  dalem55  40542  cdlema1N  40606  paddclN  40657  pmapjoin  40667  dalawlem3  40688  dalawlem5  40690  dalawlem7  40692  dalawlem8  40693  dalawlem11  40696  dalawlem12  40697  lhpexle3lem  40826  4atexlemc  40884  trlnidat  40988  arglem1N  41005  cdlemd9  41021  cdleme0moN  41040  cdleme11c  41076  cdleme11h  41081  cdleme11  41085  cdleme16c  41095  cdleme16f  41098  cdlemeda  41113  cdleme20l2  41136  cdlemefs32sn1aw  41229  cdleme43fsv1snlem  41235  cdleme41sn3a  41248  cdleme32fva  41252  cdleme32b  41257  cdleme32c  41258  cdleme32e  41260  cdleme40m  41282  cdleme40n  41283  cdleme42e  41294  cdleme48d  41350  cdlemf2  41377  cdlemf  41378  cdlemg2fv2  41415  cdlemg7fvbwN  41422  cdlemg7fvN  41439  cdlemg9a  41447  cdlemg9b  41448  cdlemg10a  41455  cdlemg12b  41459  cdlemg17b  41477  cdlemg31d  41515  cdlemg33b0  41516  cdlemg33a  41521  ltrnco  41534  ltrncom  41553  cdlemh  41632  cdlemk3  41648  cdlemk12  41665  cdlemk12u  41687  cdlemkfid1N  41736  cdlemk51  41768  cdlemk54  41773  cdlemk43N  41778  cdlemk35u  41779  cdlemk55u1  41780  cdlemk39u1  41782  cdlemk19u1  41784  dia2dimlem10  41888  dvhgrp  41922  dvh0g  41926  cdlemm10N  41933  diblsmopel  41986  cdlemn4  42013  cdlemn6  42017  cdlemn7  42018  dihordlem7  42029  dihord1  42033  dihord2pre  42040  dihvalcqat  42054  dihopelvalcpre  42063  dihord5apre  42077  dihord  42079  dih1  42101  dihglbcpreN  42115  dihjatc1  42126  dihmeetlem13N  42134  dihmeetALTN  42142  dihjatcclem1  42233  baerlem3lem1  42522  domnexpgn0cl  43332  pellfundex  43654  rmxypairf1o  43679  rmxycomplete  43685  rmxyneg  43688  rmxyadd  43689  rmxy1  43690  rmxy0  43691  jm2.22  43763  proot1mul  43962  deg1mhm  43968  stoweidlem7  46762  stoweidlem36  46791