Theorem syl122anc 1376

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 515	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1372	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  divdiv32d  11430  divcan5d  11431  divcan7d  11433  divdiv1d  11436  divdiv2d  11437  seqcoll  13818  cau3lem  14706  eqsqrtd  14719  isercolllem2  15014  isercoll  15016  summolem2a  15064  divrcnv  15199  prodmolem2a  15280  prmind2  16019  divnumden  16078  pceulem  16172  pcqmul  16180  pcqdiv  16184  pcexp  16186  pcaddlem  16214  pcbc  16226  prmodvdslcmf  16373  latledi  17691  latjjdi  17705  latjjdir  17706  sylow1lem1  18715  sylow1lem5  18719  efgred2  18871  abladdsub4  18927  ablpnpcan  18933  ghmplusg  18959  frgpnabllem2  18987  isabvd  19584  lmodvs1  19655  lspsolvlem  19907  frgpcyg  20265  ip2di  20330  evlslem1  20754  mdetuni0  21226  cpmadugsumlemB  21479  elptr2  22179  blss2ps  23010  blss2  23011  blssps  23031  blss  23032  xmeter  23040  metdcnlem  23441  lebnumii  23571  minveclem2  24030  pjthlem1  24041  volfiniun  24151  dvfsumrlimge0  24633  lgsdi  25918  ax5seglem3  26725  ax5seglem6  26728  axcontlem8  26765  eengtrkg  26780  vacn  28477  minvecolem2  28658  minvecolem4  28663  disjabrex  30345  disjabrexf  30346  2ndresdju  30411  fnpreimac  30434  slmdvs1  30898  slmd0vs  30902  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  orngmullt  30933  suborng  30939  isprmidlc  31031  madjusmdetlem1  31180  cgrcomand  33565  cgrcomr  33571  cgrcomland  33573  cgrcomrand  33574  cgrtriv  33576  cgrid2  33577  ofscom  33581  cgrextend  33582  segconeq  33584  btwntriv2  33586  btwnexch3and  33595  btwnouttr2  33596  btwnouttr  33598  btwnexch  33599  btwnexchand  33600  btwndiff  33601  ifscgr  33618  cgrsub  33619  cgrxfr  33629  lineext  33650  endofsegid  33659  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem7  33667  btwnconn1lem8  33668  btwnconn1lem10  33670  btwnconn1lem11  33671  btwnconn1lem13  33673  btwnconn1lem14  33674  btwnconn3  33677  midofsegid  33678  segcon2  33679  brsegle2  33683  seglecgr12im  33684  seglecgr12  33685  seglerflx  33686  seglemin  33687  segletr  33688  btwnsegle  33691  colinbtwnle  33692  btwnoutside  33699  broutsideof3  33700  outsideoftr  33703  outsideofeq  33704  outsidele  33706  lineunray  33721  lineelsb2  33722  lfladdcl  36367  lshpkrlem4  36409  latmmdiN  36530  latmmdir  36531  hlatj4  36670  4atlem4b  36896  4atlem11  36905  4atlem12  36908  dalem2  36957  dalem-cly  36967  dalem10  36969  dalem23  36992  dalem38  37006  dalem44  37012  dalem55  37023  cdlema1N  37087  paddclN  37138  pmapjoin  37148  dalawlem3  37169  dalawlem5  37171  dalawlem7  37173  dalawlem8  37174  dalawlem11  37177  dalawlem12  37178  lhpexle3lem  37307  4atexlemc  37365  trlnidat  37469  arglem1N  37486  cdlemd9  37502  cdleme0moN  37521  cdleme11c  37557  cdleme11h  37562  cdleme11  37566  cdleme16c  37576  cdleme16f  37579  cdlemeda  37594  cdleme20l2  37617  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme41sn3a  37729  cdleme32fva  37733  cdleme32b  37738  cdleme32c  37739  cdleme32e  37741  cdleme40m  37763  cdleme40n  37764  cdleme42e  37775  cdleme48d  37831  cdlemf2  37858  cdlemf  37859  cdlemg2fv2  37896  cdlemg7fvbwN  37903  cdlemg7fvN  37920  cdlemg9a  37928  cdlemg9b  37929  cdlemg10a  37936  cdlemg12b  37940  cdlemg17b  37958  cdlemg31d  37996  cdlemg33b0  37997  cdlemg33a  38002  ltrnco  38015  ltrncom  38034  cdlemh  38113  cdlemk3  38129  cdlemk12  38146  cdlemk12u  38168  cdlemkfid1N  38217  cdlemk51  38249  cdlemk54  38254  cdlemk43N  38259  cdlemk35u  38260  cdlemk55u1  38261  cdlemk39u1  38263  cdlemk19u1  38265  dia2dimlem10  38369  dvhgrp  38403  dvh0g  38407  cdlemm10N  38414  diblsmopel  38467  cdlemn4  38494  cdlemn6  38498  cdlemn7  38499  dihordlem7  38510  dihord1  38514  dihord2pre  38521  dihvalcqat  38535  dihopelvalcpre  38544  dihord5apre  38558  dihord  38560  dih1  38582  dihglbcpreN  38596  dihjatc1  38607  dihmeetlem13N  38615  dihmeetALTN  38623  dihjatcclem1  38714  baerlem3lem1  39003  pellfundex  39827  rmxypairf1o  39852  rmxycomplete  39858  rmxyneg  39861  rmxyadd  39862  rmxy1  39863  rmxy0  39864  jm2.22  39936  proot1mul  40143  deg1mhm  40151  stoweidlem7  42649  stoweidlem36  42678