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  11983  divcan5d  11984  divcan7d  11986  divdiv1d  11989  divdiv2d  11990  seqcoll  14429  cau3lem  15321  eqsqrtd  15334  isercolllem2  15632  isercoll  15634  summolem2a  15681  divrcnv  15818  prodmolem2a  15900  prmind2  16655  divnumden  16718  pceulem  16816  pcqmul  16824  pcqdiv  16828  pcexp  16830  pcaddlem  16859  pcbc  16871  prmodvdslcmf  17018  latledi  18436  latjjdi  18450  latjjdir  18451  sylow1lem1  19528  sylow1lem5  19532  efgred2  19683  abladdsub4  19741  ablpnpcan  19749  ghmplusg  19776  frgpnabllem2  19804  isdomn4  20625  isabvd  20721  lmodvs1  20796  lspsolvlem  21052  frgpcyg  21483  ip2di  21550  evlslem1  21989  mdetuni0  22508  cpmadugsumlemB  22761  elptr2  23461  blss2ps  24291  blss2  24292  blssps  24312  blss  24313  xmeter  24321  metdcnlem  24725  lebnumii  24865  minveclem2  25326  pjthlem1  25337  volfiniun  25448  dvfsumrlimge0  25937  lgsdi  27245  cofcut1d  27829  ax5seglem3  28858  ax5seglem6  28861  axcontlem8  28898  eengtrkg  28913  vacn  30623  minvecolem2  30804  minvecolem4  30809  disjabrex  32511  disjabrexf  32512  2ndresdju  32573  fnpreimac  32595  cmn4d  32973  slmdvs1  33173  slmd0vs  33177  rlocaddval  33219  domnprodn0  33226  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  orngmullt  33287  suborng  33293  isprmidlc  33418  ssdifidlprm  33429  q1pdir  33568  madjusmdetlem1  33817  cgrcomand  35979  cgrcomr  35985  cgrcomland  35987  cgrcomrand  35988  cgrtriv  35990  cgrid2  35991  ofscom  35995  cgrextend  35996  segconeq  35998  btwntriv2  36000  btwnexch3and  36009  btwnouttr2  36010  btwnouttr  36012  btwnexch  36013  btwnexchand  36014  btwndiff  36015  ifscgr  36032  cgrsub  36033  cgrxfr  36043  lineext  36064  endofsegid  36073  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem7  36081  btwnconn1lem8  36082  btwnconn1lem10  36084  btwnconn1lem11  36085  btwnconn1lem13  36087  btwnconn1lem14  36088  btwnconn3  36091  midofsegid  36092  segcon2  36093  brsegle2  36097  seglecgr12im  36098  seglecgr12  36099  seglerflx  36100  seglemin  36101  segletr  36102  btwnsegle  36105  colinbtwnle  36106  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  outsideofeq  36118  outsidele  36120  lineunray  36135  lineelsb2  36136  lfladdcl  39064  lshpkrlem4  39106  latmmdiN  39227  latmmdir  39228  hlatj4  39367  4atlem4b  39594  4atlem11  39603  4atlem12  39606  dalem2  39655  dalem-cly  39665  dalem10  39667  dalem23  39690  dalem38  39704  dalem44  39710  dalem55  39721  cdlema1N  39785  paddclN  39836  pmapjoin  39846  dalawlem3  39867  dalawlem5  39869  dalawlem7  39871  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  lhpexle3lem  40005  4atexlemc  40063  trlnidat  40167  arglem1N  40184  cdlemd9  40200  cdleme0moN  40219  cdleme11c  40255  cdleme11h  40260  cdleme11  40264  cdleme16c  40274  cdleme16f  40277  cdlemeda  40292  cdleme20l2  40315  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32fva  40431  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme40m  40461  cdleme40n  40462  cdleme42e  40473  cdleme48d  40529  cdlemf2  40556  cdlemf  40557  cdlemg2fv2  40594  cdlemg7fvbwN  40601  cdlemg7fvN  40618  cdlemg9a  40626  cdlemg9b  40627  cdlemg10a  40634  cdlemg12b  40638  cdlemg17b  40656  cdlemg31d  40694  cdlemg33b0  40695  cdlemg33a  40700  ltrnco  40713  ltrncom  40732  cdlemh  40811  cdlemk3  40827  cdlemk12  40844  cdlemk12u  40866  cdlemkfid1N  40915  cdlemk51  40947  cdlemk54  40952  cdlemk43N  40957  cdlemk35u  40958  cdlemk55u1  40959  cdlemk39u1  40961  cdlemk19u1  40963  dia2dimlem10  41067  dvhgrp  41101  dvh0g  41105  cdlemm10N  41112  diblsmopel  41165  cdlemn4  41192  cdlemn6  41196  cdlemn7  41197  dihordlem7  41208  dihord1  41212  dihord2pre  41219  dihvalcqat  41233  dihopelvalcpre  41242  dihord5apre  41256  dihord  41258  dih1  41280  dihglbcpreN  41294  dihjatc1  41305  dihmeetlem13N  41313  dihmeetALTN  41321  dihjatcclem1  41412  baerlem3lem1  41701  domnexpgn0cl  42511  pellfundex  42874  rmxypairf1o  42900  rmxycomplete  42906  rmxyneg  42909  rmxyadd  42910  rmxy1  42911  rmxy0  42912  jm2.22  42984  proot1mul  43183  deg1mhm  43189  stoweidlem7  46005  stoweidlem36  46034