Theorem syl122anc 1377

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  divdiv32d  11706  divcan5d  11707  divcan7d  11709  divdiv1d  11712  divdiv2d  11713  seqcoll  14106  cau3lem  14994  eqsqrtd  15007  isercolllem2  15305  isercoll  15307  summolem2a  15355  divrcnv  15492  prodmolem2a  15572  prmind2  16318  divnumden  16380  pceulem  16474  pcqmul  16482  pcqdiv  16486  pcexp  16488  pcaddlem  16517  pcbc  16529  prmodvdslcmf  16676  latledi  18110  latjjdi  18124  latjjdir  18125  sylow1lem1  19118  sylow1lem5  19122  efgred2  19274  abladdsub4  19330  ablpnpcan  19336  ghmplusg  19362  frgpnabllem2  19390  isabvd  19995  lmodvs1  20066  lspsolvlem  20319  frgpcyg  20693  ip2di  20758  evlslem1  21202  mdetuni0  21678  cpmadugsumlemB  21931  elptr2  22633  blss2ps  23464  blss2  23465  blssps  23485  blss  23486  xmeter  23494  metdcnlem  23905  lebnumii  24035  minveclem2  24495  pjthlem1  24506  volfiniun  24616  dvfsumrlimge0  25099  lgsdi  26387  ax5seglem3  27202  ax5seglem6  27205  axcontlem8  27242  eengtrkg  27257  vacn  28957  minvecolem2  29138  minvecolem4  29143  disjabrex  30822  disjabrexf  30823  2ndresdju  30887  fnpreimac  30910  slmdvs1  31375  slmd0vs  31379  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  orngmullt  31410  suborng  31416  isprmidlc  31525  madjusmdetlem1  31679  cgrcomand  34220  cgrcomr  34226  cgrcomland  34228  cgrcomrand  34229  cgrtriv  34231  cgrid2  34232  ofscom  34236  cgrextend  34237  segconeq  34239  btwntriv2  34241  btwnexch3and  34250  btwnouttr2  34251  btwnouttr  34253  btwnexch  34254  btwnexchand  34255  btwndiff  34256  ifscgr  34273  cgrsub  34274  cgrxfr  34284  lineext  34305  endofsegid  34314  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem7  34322  btwnconn1lem8  34323  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn1lem13  34328  btwnconn1lem14  34329  btwnconn3  34332  midofsegid  34333  segcon2  34334  brsegle2  34338  seglecgr12im  34339  seglecgr12  34340  seglerflx  34341  seglemin  34342  segletr  34343  btwnsegle  34346  colinbtwnle  34347  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  outsideofeq  34359  outsidele  34361  lineunray  34376  lineelsb2  34377  lfladdcl  37012  lshpkrlem4  37054  latmmdiN  37175  latmmdir  37176  hlatj4  37315  4atlem4b  37541  4atlem11  37550  4atlem12  37553  dalem2  37602  dalem-cly  37612  dalem10  37614  dalem23  37637  dalem38  37651  dalem44  37657  dalem55  37668  cdlema1N  37732  paddclN  37783  pmapjoin  37793  dalawlem3  37814  dalawlem5  37816  dalawlem7  37818  dalawlem8  37819  dalawlem11  37822  dalawlem12  37823  lhpexle3lem  37952  4atexlemc  38010  trlnidat  38114  arglem1N  38131  cdlemd9  38147  cdleme0moN  38166  cdleme11c  38202  cdleme11h  38207  cdleme11  38211  cdleme16c  38221  cdleme16f  38224  cdlemeda  38239  cdleme20l2  38262  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32fva  38378  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme40m  38408  cdleme40n  38409  cdleme42e  38420  cdleme48d  38476  cdlemf2  38503  cdlemf  38504  cdlemg2fv2  38541  cdlemg7fvbwN  38548  cdlemg7fvN  38565  cdlemg9a  38573  cdlemg9b  38574  cdlemg10a  38581  cdlemg12b  38585  cdlemg17b  38603  cdlemg31d  38641  cdlemg33b0  38642  cdlemg33a  38647  ltrnco  38660  ltrncom  38679  cdlemh  38758  cdlemk3  38774  cdlemk12  38791  cdlemk12u  38813  cdlemkfid1N  38862  cdlemk51  38894  cdlemk54  38899  cdlemk43N  38904  cdlemk35u  38905  cdlemk55u1  38906  cdlemk39u1  38908  cdlemk19u1  38910  dia2dimlem10  39014  dvhgrp  39048  dvh0g  39052  cdlemm10N  39059  diblsmopel  39112  cdlemn4  39139  cdlemn6  39143  cdlemn7  39144  dihordlem7  39155  dihord1  39159  dihord2pre  39166  dihvalcqat  39180  dihopelvalcpre  39189  dihord5apre  39203  dihord  39205  dih1  39227  dihglbcpreN  39241  dihjatc1  39252  dihmeetlem13N  39260  dihmeetALTN  39268  dihjatcclem1  39359  baerlem3lem1  39648  isdomn4  40100  pellfundex  40624  rmxypairf1o  40649  rmxycomplete  40655  rmxyneg  40658  rmxyadd  40659  rmxy1  40660  rmxy0  40661  jm2.22  40733  proot1mul  40940  deg1mhm  40948  stoweidlem7  43438  stoweidlem36  43467