Theorem syl122anc 1382

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 1378	1 ⊢ (𝜑 → 𝜁)

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

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 1089

This theorem is referenced by:  divdiv32d  11954  divcan5d  11955  divcan7d  11957  divdiv1d  11960  divdiv2d  11961  seqcoll  14399  cau3lem  15290  eqsqrtd  15303  isercolllem2  15601  isercoll  15603  summolem2a  15650  divrcnv  15787  prodmolem2a  15869  prmind2  16624  divnumden  16687  pceulem  16785  pcqmul  16793  pcqdiv  16797  pcexp  16799  pcaddlem  16828  pcbc  16840  prmodvdslcmf  16987  latledi  18412  latjjdi  18426  latjjdir  18427  sylow1lem1  19539  sylow1lem5  19543  efgred2  19694  abladdsub4  19752  ablpnpcan  19760  ghmplusg  19787  frgpnabllem2  19815  isdomn4  20661  isabvd  20757  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  orngmullt  20816  suborng  20821  lmodvs1  20853  lspsolvlem  21109  frgpcyg  21540  ip2di  21608  evlslem1  22049  mdetuni0  22577  cpmadugsumlemB  22830  elptr2  23530  blss2ps  24359  blss2  24360  blssps  24380  blss  24381  xmeter  24389  metdcnlem  24793  lebnumii  24933  minveclem2  25394  pjthlem1  25405  volfiniun  25516  dvfsumrlimge0  26005  lgsdi  27313  cofcut1d  27929  ax5seglem3  29016  ax5seglem6  29019  axcontlem8  29056  eengtrkg  29071  vacn  30781  minvecolem2  30962  minvecolem4  30967  disjabrex  32668  disjabrexf  32669  2ndresdju  32738  fnpreimac  32759  cmn4d  33124  gsummulsubdishift1  33161  slmdvs1  33313  slmd0vs  33317  rlocaddval  33361  domnprodn0  33368  isprmidlc  33539  ssdifidlprm  33550  q1pdir  33695  madjusmdetlem1  34004  cgrcomand  36204  cgrcomr  36210  cgrcomland  36212  cgrcomrand  36213  cgrtriv  36215  cgrid2  36216  ofscom  36220  cgrextend  36221  segconeq  36223  btwntriv2  36225  btwnexch3and  36234  btwnouttr2  36235  btwnouttr  36237  btwnexch  36238  btwnexchand  36239  btwndiff  36240  ifscgr  36257  cgrsub  36258  cgrxfr  36268  lineext  36289  endofsegid  36298  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem7  36306  btwnconn1lem8  36307  btwnconn1lem10  36309  btwnconn1lem11  36310  btwnconn1lem13  36312  btwnconn1lem14  36313  btwnconn3  36316  midofsegid  36317  segcon2  36318  brsegle2  36322  seglecgr12im  36323  seglecgr12  36324  seglerflx  36325  seglemin  36326  segletr  36327  btwnsegle  36330  colinbtwnle  36331  btwnoutside  36338  broutsideof3  36339  outsideoftr  36342  outsideofeq  36343  outsidele  36345  lineunray  36360  lineelsb2  36361  lfladdcl  39441  lshpkrlem4  39483  latmmdiN  39604  latmmdir  39605  hlatj4  39744  4atlem4b  39970  4atlem11  39979  4atlem12  39982  dalem2  40031  dalem-cly  40041  dalem10  40043  dalem23  40066  dalem38  40080  dalem44  40086  dalem55  40097  cdlema1N  40161  paddclN  40212  pmapjoin  40222  dalawlem3  40243  dalawlem5  40245  dalawlem7  40247  dalawlem8  40248  dalawlem11  40251  dalawlem12  40252  lhpexle3lem  40381  4atexlemc  40439  trlnidat  40543  arglem1N  40560  cdlemd9  40576  cdleme0moN  40595  cdleme11c  40631  cdleme11h  40636  cdleme11  40640  cdleme16c  40650  cdleme16f  40653  cdlemeda  40668  cdleme20l2  40691  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdleme41sn3a  40803  cdleme32fva  40807  cdleme32b  40812  cdleme32c  40813  cdleme32e  40815  cdleme40m  40837  cdleme40n  40838  cdleme42e  40849  cdleme48d  40905  cdlemf2  40932  cdlemf  40933  cdlemg2fv2  40970  cdlemg7fvbwN  40977  cdlemg7fvN  40994  cdlemg9a  41002  cdlemg9b  41003  cdlemg10a  41010  cdlemg12b  41014  cdlemg17b  41032  cdlemg31d  41070  cdlemg33b0  41071  cdlemg33a  41076  ltrnco  41089  ltrncom  41108  cdlemh  41187  cdlemk3  41203  cdlemk12  41220  cdlemk12u  41242  cdlemkfid1N  41291  cdlemk51  41323  cdlemk54  41328  cdlemk43N  41333  cdlemk35u  41334  cdlemk55u1  41335  cdlemk39u1  41337  cdlemk19u1  41339  dia2dimlem10  41443  dvhgrp  41477  dvh0g  41481  cdlemm10N  41488  diblsmopel  41541  cdlemn4  41568  cdlemn6  41572  cdlemn7  41573  dihordlem7  41584  dihord1  41588  dihord2pre  41595  dihvalcqat  41609  dihopelvalcpre  41618  dihord5apre  41632  dihord  41634  dih1  41656  dihglbcpreN  41670  dihjatc1  41681  dihmeetlem13N  41689  dihmeetALTN  41697  dihjatcclem1  41788  baerlem3lem1  42077  domnexpgn0cl  42887  pellfundex  43237  rmxypairf1o  43262  rmxycomplete  43268  rmxyneg  43271  rmxyadd  43272  rmxy1  43273  rmxy0  43274  jm2.22  43346  proot1mul  43545  deg1mhm  43551  stoweidlem7  46359  stoweidlem36  46388