Theorem syl122anc 1407

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 1403	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  12148  divcan5d  12149  divcan7d  12151  divdiv1d  12154  divdiv2d  12155  seqcoll  14639  cau3lem  15554  eqsqrtd  15567  isercolllem2  15865  isercoll  15867  summolem2a  15913  divrcnv  16053  prodmolem2a  16133  prmind2  16892  divnumden  16956  pceulem  17055  pcqmul  17063  pcqdiv  17067  pcexp  17069  pcaddlem  17098  pcbc  17110  prmodvdslcmf  17257  latledi  18683  latjjdi  18697  latjjdir  18698  sylow1lem1  19845  sylow1lem5  19849  efgred2  20000  abladdsub4  20058  ablpnpcan  20066  ghmplusg  20093  frgpnabllem2  20121  isdomn4  21000  isabvd  21102  orngsqr  21156  ornglmulle  21157  orngrmulle  21158  orngmullt  21161  suborng  21166  lmodvs1  21198  lspsolvlem  21453  isprmidlc  21661  ssdifidlprm  21675  frgpcyg  21912  ip2di  21980  evlslem1  22424  mdetuni0  22969  cpmadugsumlemB  23225  elptr2  23926  blss2ps  24755  blss2  24756  blssps  24776  blss  24777  xmeter  24785  metdcnlem  25189  lebnumii  25320  minveclem2  25780  pjthlem1  25791  volfiniun  25901  dvfsumrlimge0  26383  lgsdi  27694  cofcut1d  28340  prlngeq  29468  ax5seglem3  29542  ax5seglem6  29545  axcontlem8  29582  eengtrkg  29597  vacn  31329  minvecolem2  31510  minvecolem4  31515  disjabrex  33251  disjabrexf  33252  2ndresdju  33318  fnpreimac  33339  cmn4d  33669  gsummulsubdishift1  33705  slmdvs1  33857  slmd0vs  33861  rlocaddval  33906  domnprodn0  33915  q1pdir  34218  madjusmdetlem1  34542  cgrcomand  36947  cgrcomr  36953  cgrcomland  36955  cgrcomrand  36956  cgrtriv  36958  cgrid2  36959  ofscom  36963  cgrextend  36964  segconeq  36966  btwntriv2  36968  btwnexch3and  36977  btwnouttr2  36978  btwnouttr  36980  btwnexch  36981  btwnexchand  36982  btwndiff  36983  ifscgr  37000  cgrsub  37001  cgrxfr  37011  lineext  37032  endofsegid  37041  btwnconn1lem2  37044  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem5  37047  btwnconn1lem7  37049  btwnconn1lem8  37050  btwnconn1lem10  37052  btwnconn1lem11  37053  btwnconn1lem13  37055  btwnconn1lem14  37056  btwnconn3  37059  midofsegid  37060  segcon2  37061  brsegle2  37065  seglecgr12im  37066  seglecgr12  37067  seglerflx  37068  seglemin  37069  segletr  37070  btwnsegle  37073  colinbtwnle  37074  btwnoutside  37081  broutsideof3  37082  outsideoftr  37085  outsideofeq  37086  outsidele  37088  lineunray  37103  lineelsb2  37104  lfladdcl  40331  lshpkrlem4  40373  latmmdiN  40494  latmmdir  40495  hlatj4  40634  4atlem4b  40860  4atlem11  40869  4atlem12  40872  dalem2  40921  dalem-cly  40931  dalem10  40933  dalem23  40956  dalem38  40970  dalem44  40976  dalem55  40987  cdlema1N  41051  paddclN  41102  pmapjoin  41112  dalawlem3  41133  dalawlem5  41135  dalawlem7  41137  dalawlem8  41138  dalawlem11  41141  dalawlem12  41142  lhpexle3lem  41271  4atexlemc  41329  trlnidat  41433  arglem1N  41450  cdlemd9  41466  cdleme0moN  41485  cdleme11c  41521  cdleme11h  41526  cdleme11  41530  cdleme16c  41540  cdleme16f  41543  cdlemeda  41558  cdleme20l2  41581  cdlemefs32sn1aw  41674  cdleme43fsv1snlem  41680  cdleme41sn3a  41693  cdleme32fva  41697  cdleme32b  41702  cdleme32c  41703  cdleme32e  41705  cdleme40m  41727  cdleme40n  41728  cdleme42e  41739  cdleme48d  41795  cdlemf2  41822  cdlemf  41823  cdlemg2fv2  41860  cdlemg7fvbwN  41867  cdlemg7fvN  41884  cdlemg9a  41892  cdlemg9b  41893  cdlemg10a  41900  cdlemg12b  41904  cdlemg17b  41922  cdlemg31d  41960  cdlemg33b0  41961  cdlemg33a  41966  ltrnco  41979  ltrncom  41998  cdlemh  42077  cdlemk3  42093  cdlemk12  42110  cdlemk12u  42132  cdlemkfid1N  42181  cdlemk51  42213  cdlemk54  42218  cdlemk43N  42223  cdlemk35u  42224  cdlemk55u1  42225  cdlemk39u1  42227  cdlemk19u1  42229  dia2dimlem10  42333  dvhgrp  42367  dvh0g  42371  cdlemm10N  42378  diblsmopel  42431  cdlemn4  42458  cdlemn6  42462  cdlemn7  42463  dihordlem7  42474  dihord1  42478  dihord2pre  42485  dihvalcqat  42499  dihopelvalcpre  42508  dihord5apre  42522  dihord  42524  dih1  42546  dihglbcpreN  42560  dihjatc1  42571  dihmeetlem13N  42579  dihmeetALTN  42587  dihjatcclem1  42678  baerlem3lem1  42967  domnexpgn0cl  43788  pellfundex  44097  rmxypairf1o  44122  rmxycomplete  44128  rmxyneg  44131  rmxyadd  44132  rmxy1  44133  rmxy0  44134  jm2.22  44206  proot1mul  44399  deg1mhm  44405  stoweidlem7  47232  stoweidlem36  47261