Theorem syl122anc 1375

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  divdiv32d  11441  divcan5d  11442  divcan7d  11444  divdiv1d  11447  divdiv2d  11448  seqcoll  13823  cau3lem  14714  eqsqrtd  14727  isercolllem2  15022  isercoll  15024  summolem2a  15072  divrcnv  15207  prodmolem2a  15288  prmind2  16029  divnumden  16088  pceulem  16182  pcqmul  16190  pcqdiv  16194  pcexp  16196  pcaddlem  16224  pcbc  16236  prmodvdslcmf  16383  latledi  17699  latjjdi  17713  latjjdir  17714  sylow1lem1  18723  sylow1lem5  18727  efgred2  18879  abladdsub4  18934  ablpnpcan  18940  ghmplusg  18966  frgpnabllem2  18994  isabvd  19591  lmodvs1  19662  lspsolvlem  19914  evlslem1  20295  frgpcyg  20720  ip2di  20785  mdetuni0  21230  cpmadugsumlemB  21482  elptr2  22182  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  xmeter  23043  metdcnlem  23444  lebnumii  23570  minveclem2  24029  pjthlem1  24040  volfiniun  24148  dvfsumrlimge0  24627  lgsdi  25910  ax5seglem3  26717  ax5seglem6  26720  axcontlem8  26757  eengtrkg  26772  vacn  28471  minvecolem2  28652  minvecolem4  28657  disjabrex  30332  disjabrexf  30333  fnpreimac  30416  slmdvs1  30848  slmd0vs  30852  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  orngmullt  30882  suborng  30888  isprmidlc  30963  madjusmdetlem1  31092  cgrcomand  33452  cgrcomr  33458  cgrcomland  33460  cgrcomrand  33461  cgrtriv  33463  cgrid2  33464  ofscom  33468  cgrextend  33469  segconeq  33471  btwntriv2  33473  btwnexch3and  33482  btwnouttr2  33483  btwnouttr  33485  btwnexch  33486  btwnexchand  33487  btwndiff  33488  ifscgr  33505  cgrsub  33506  cgrxfr  33516  lineext  33537  endofsegid  33546  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem7  33554  btwnconn1lem8  33555  btwnconn1lem10  33557  btwnconn1lem11  33558  btwnconn1lem13  33560  btwnconn1lem14  33561  btwnconn3  33564  midofsegid  33565  segcon2  33566  brsegle2  33570  seglecgr12im  33571  seglecgr12  33572  seglerflx  33573  seglemin  33574  segletr  33575  btwnsegle  33578  colinbtwnle  33579  btwnoutside  33586  broutsideof3  33587  outsideoftr  33590  outsideofeq  33591  outsidele  33593  lineunray  33608  lineelsb2  33609  lfladdcl  36222  lshpkrlem4  36264  latmmdiN  36385  latmmdir  36386  hlatj4  36525  4atlem4b  36751  4atlem11  36760  4atlem12  36763  dalem2  36812  dalem-cly  36822  dalem10  36824  dalem23  36847  dalem38  36861  dalem44  36867  dalem55  36878  cdlema1N  36942  paddclN  36993  pmapjoin  37003  dalawlem3  37024  dalawlem5  37026  dalawlem7  37028  dalawlem8  37029  dalawlem11  37032  dalawlem12  37033  lhpexle3lem  37162  4atexlemc  37220  trlnidat  37324  arglem1N  37341  cdlemd9  37357  cdleme0moN  37376  cdleme11c  37412  cdleme11h  37417  cdleme11  37421  cdleme16c  37431  cdleme16f  37434  cdlemeda  37449  cdleme20l2  37472  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdleme41sn3a  37584  cdleme32fva  37588  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme40m  37618  cdleme40n  37619  cdleme42e  37630  cdleme48d  37686  cdlemf2  37713  cdlemf  37714  cdlemg2fv2  37751  cdlemg7fvbwN  37758  cdlemg7fvN  37775  cdlemg9a  37783  cdlemg9b  37784  cdlemg10a  37791  cdlemg12b  37795  cdlemg17b  37813  cdlemg31d  37851  cdlemg33b0  37852  cdlemg33a  37857  ltrnco  37870  ltrncom  37889  cdlemh  37968  cdlemk3  37984  cdlemk12  38001  cdlemk12u  38023  cdlemkfid1N  38072  cdlemk51  38104  cdlemk54  38109  cdlemk43N  38114  cdlemk35u  38115  cdlemk55u1  38116  cdlemk39u1  38118  cdlemk19u1  38120  dia2dimlem10  38224  dvhgrp  38258  dvh0g  38262  cdlemm10N  38269  diblsmopel  38322  cdlemn4  38349  cdlemn6  38353  cdlemn7  38354  dihordlem7  38365  dihord1  38369  dihord2pre  38376  dihvalcqat  38390  dihopelvalcpre  38399  dihord5apre  38413  dihord  38415  dih1  38437  dihglbcpreN  38451  dihjatc1  38462  dihmeetlem13N  38470  dihmeetALTN  38478  dihjatcclem1  38569  baerlem3lem1  38858  pellfundex  39503  rmxypairf1o  39528  rmxycomplete  39534  rmxyneg  39537  rmxyadd  39538  rmxy1  39539  rmxy0  39540  jm2.22  39612  proot1mul  39819  deg1mhm  39827  stoweidlem7  42312  stoweidlem36  42341