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  12040  divcan5d  12041  divcan7d  12043  divdiv1d  12046  divdiv2d  12047  seqcoll  14480  cau3lem  15371  eqsqrtd  15384  isercolllem2  15680  isercoll  15682  summolem2a  15729  divrcnv  15866  prodmolem2a  15948  prmind2  16702  divnumden  16765  pceulem  16863  pcqmul  16871  pcqdiv  16875  pcexp  16877  pcaddlem  16906  pcbc  16918  prmodvdslcmf  17065  latledi  18485  latjjdi  18499  latjjdir  18500  sylow1lem1  19577  sylow1lem5  19581  efgred2  19732  abladdsub4  19790  ablpnpcan  19798  ghmplusg  19825  frgpnabllem2  19853  isdomn4  20674  isabvd  20770  lmodvs1  20845  lspsolvlem  21101  frgpcyg  21532  ip2di  21599  evlslem1  22038  mdetuni0  22557  cpmadugsumlemB  22810  elptr2  23510  blss2ps  24340  blss2  24341  blssps  24361  blss  24362  xmeter  24370  metdcnlem  24774  lebnumii  24914  minveclem2  25376  pjthlem1  25387  volfiniun  25498  dvfsumrlimge0  25987  lgsdi  27295  cofcut1d  27872  ax5seglem3  28856  ax5seglem6  28859  axcontlem8  28896  eengtrkg  28911  vacn  30621  minvecolem2  30802  minvecolem4  30807  disjabrex  32509  disjabrexf  32510  2ndresdju  32573  fnpreimac  32595  cmn4d  32973  slmdvs1  33163  slmd0vs  33167  rlocaddval  33209  domnprodn0  33216  orngsqr  33272  ornglmulle  33273  orngrmulle  33274  orngmullt  33277  suborng  33283  isprmidlc  33408  ssdifidlprm  33419  q1pdir  33558  madjusmdetlem1  33804  cgrcomand  35955  cgrcomr  35961  cgrcomland  35963  cgrcomrand  35964  cgrtriv  35966  cgrid2  35967  ofscom  35971  cgrextend  35972  segconeq  35974  btwntriv2  35976  btwnexch3and  35985  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  btwnexchand  35990  btwndiff  35991  ifscgr  36008  cgrsub  36009  cgrxfr  36019  lineext  36040  endofsegid  36049  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  midofsegid  36068  segcon2  36069  brsegle2  36073  seglecgr12im  36074  seglecgr12  36075  seglerflx  36076  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsideofeq  36094  outsidele  36096  lineunray  36111  lineelsb2  36112  lfladdcl  39035  lshpkrlem4  39077  latmmdiN  39198  latmmdir  39199  hlatj4  39338  4atlem4b  39565  4atlem11  39574  4atlem12  39577  dalem2  39626  dalem-cly  39636  dalem10  39638  dalem23  39661  dalem38  39675  dalem44  39681  dalem55  39692  cdlema1N  39756  paddclN  39807  pmapjoin  39817  dalawlem3  39838  dalawlem5  39840  dalawlem7  39842  dalawlem8  39843  dalawlem11  39846  dalawlem12  39847  lhpexle3lem  39976  4atexlemc  40034  trlnidat  40138  arglem1N  40155  cdlemd9  40171  cdleme0moN  40190  cdleme11c  40226  cdleme11h  40231  cdleme11  40235  cdleme16c  40245  cdleme16f  40248  cdlemeda  40263  cdleme20l2  40286  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32fva  40402  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme40m  40432  cdleme40n  40433  cdleme42e  40444  cdleme48d  40500  cdlemf2  40527  cdlemf  40528  cdlemg2fv2  40565  cdlemg7fvbwN  40572  cdlemg7fvN  40589  cdlemg9a  40597  cdlemg9b  40598  cdlemg10a  40605  cdlemg12b  40609  cdlemg17b  40627  cdlemg31d  40665  cdlemg33b0  40666  cdlemg33a  40671  ltrnco  40684  ltrncom  40703  cdlemh  40782  cdlemk3  40798  cdlemk12  40815  cdlemk12u  40837  cdlemkfid1N  40886  cdlemk51  40918  cdlemk54  40923  cdlemk43N  40928  cdlemk35u  40929  cdlemk55u1  40930  cdlemk39u1  40932  cdlemk19u1  40934  dia2dimlem10  41038  dvhgrp  41072  dvh0g  41076  cdlemm10N  41083  diblsmopel  41136  cdlemn4  41163  cdlemn6  41167  cdlemn7  41168  dihordlem7  41179  dihord1  41183  dihord2pre  41190  dihvalcqat  41204  dihopelvalcpre  41213  dihord5apre  41227  dihord  41229  dih1  41251  dihglbcpreN  41265  dihjatc1  41276  dihmeetlem13N  41284  dihmeetALTN  41292  dihjatcclem1  41383  baerlem3lem1  41672  domnexpgn0cl  42493  pellfundex  42856  rmxypairf1o  42882  rmxycomplete  42888  rmxyneg  42891  rmxyadd  42892  rmxy1  42893  rmxy0  42894  jm2.22  42966  proot1mul  43165  deg1mhm  43171  stoweidlem7  45984  stoweidlem36  46013