Theorem syl122anc 1379

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  divdiv32d  11997  divcan5d  11998  divcan7d  12000  divdiv1d  12003  divdiv2d  12004  seqcoll  14407  cau3lem  15283  eqsqrtd  15296  isercolllem2  15594  isercoll  15596  summolem2a  15643  divrcnv  15780  prodmolem2a  15860  prmind2  16604  divnumden  16666  pceulem  16760  pcqmul  16768  pcqdiv  16772  pcexp  16774  pcaddlem  16803  pcbc  16815  prmodvdslcmf  16962  latledi  18412  latjjdi  18426  latjjdir  18427  sylow1lem1  19430  sylow1lem5  19434  efgred2  19585  abladdsub4  19642  ablpnpcan  19648  ghmplusg  19674  frgpnabllem2  19702  isabvd  20377  lmodvs1  20449  lspsolvlem  20704  frgpcyg  21062  ip2di  21127  evlslem1  21574  mdetuni0  22052  cpmadugsumlemB  22305  elptr2  23007  blss2ps  23838  blss2  23839  blssps  23859  blss  23860  xmeter  23868  metdcnlem  24281  lebnumii  24411  minveclem2  24872  pjthlem1  24883  volfiniun  24993  dvfsumrlimge0  25476  lgsdi  26764  cofcut1d  27328  ax5seglem3  28054  ax5seglem6  28057  axcontlem8  28094  eengtrkg  28109  vacn  29810  minvecolem2  29991  minvecolem4  29996  disjabrex  31678  disjabrexf  31679  2ndresdju  31743  fnpreimac  31765  slmdvs1  32236  slmd0vs  32240  orngsqr  32284  ornglmulle  32285  orngrmulle  32286  orngmullt  32289  suborng  32295  isprmidlc  32415  madjusmdetlem1  32636  cgrcomand  34791  cgrcomr  34797  cgrcomland  34799  cgrcomrand  34800  cgrtriv  34802  cgrid2  34803  ofscom  34807  cgrextend  34808  segconeq  34810  btwntriv2  34812  btwnexch3and  34821  btwnouttr2  34822  btwnouttr  34824  btwnexch  34825  btwnexchand  34826  btwndiff  34827  ifscgr  34844  cgrsub  34845  cgrxfr  34855  lineext  34876  endofsegid  34885  btwnconn1lem2  34888  btwnconn1lem3  34889  btwnconn1lem4  34890  btwnconn1lem5  34891  btwnconn1lem7  34893  btwnconn1lem8  34894  btwnconn1lem10  34896  btwnconn1lem11  34897  btwnconn1lem13  34899  btwnconn1lem14  34900  btwnconn3  34903  midofsegid  34904  segcon2  34905  brsegle2  34909  seglecgr12im  34910  seglecgr12  34911  seglerflx  34912  seglemin  34913  segletr  34914  btwnsegle  34917  colinbtwnle  34918  btwnoutside  34925  broutsideof3  34926  outsideoftr  34929  outsideofeq  34930  outsidele  34932  lineunray  34947  lineelsb2  34948  lfladdcl  37744  lshpkrlem4  37786  latmmdiN  37907  latmmdir  37908  hlatj4  38047  4atlem4b  38274  4atlem11  38283  4atlem12  38286  dalem2  38335  dalem-cly  38345  dalem10  38347  dalem23  38370  dalem38  38384  dalem44  38390  dalem55  38401  cdlema1N  38465  paddclN  38516  pmapjoin  38526  dalawlem3  38547  dalawlem5  38549  dalawlem7  38551  dalawlem8  38552  dalawlem11  38555  dalawlem12  38556  lhpexle3lem  38685  4atexlemc  38743  trlnidat  38847  arglem1N  38864  cdlemd9  38880  cdleme0moN  38899  cdleme11c  38935  cdleme11h  38940  cdleme11  38944  cdleme16c  38954  cdleme16f  38957  cdlemeda  38972  cdleme20l2  38995  cdlemefs32sn1aw  39088  cdleme43fsv1snlem  39094  cdleme41sn3a  39107  cdleme32fva  39111  cdleme32b  39116  cdleme32c  39117  cdleme32e  39119  cdleme40m  39141  cdleme40n  39142  cdleme42e  39153  cdleme48d  39209  cdlemf2  39236  cdlemf  39237  cdlemg2fv2  39274  cdlemg7fvbwN  39281  cdlemg7fvN  39298  cdlemg9a  39306  cdlemg9b  39307  cdlemg10a  39314  cdlemg12b  39318  cdlemg17b  39336  cdlemg31d  39374  cdlemg33b0  39375  cdlemg33a  39380  ltrnco  39393  ltrncom  39412  cdlemh  39491  cdlemk3  39507  cdlemk12  39524  cdlemk12u  39546  cdlemkfid1N  39595  cdlemk51  39627  cdlemk54  39632  cdlemk43N  39637  cdlemk35u  39638  cdlemk55u1  39639  cdlemk39u1  39641  cdlemk19u1  39643  dia2dimlem10  39747  dvhgrp  39781  dvh0g  39785  cdlemm10N  39792  diblsmopel  39845  cdlemn4  39872  cdlemn6  39876  cdlemn7  39877  dihordlem7  39888  dihord1  39892  dihord2pre  39899  dihvalcqat  39913  dihopelvalcpre  39922  dihord5apre  39936  dihord  39938  dih1  39960  dihglbcpreN  39974  dihjatc1  39985  dihmeetlem13N  39993  dihmeetALTN  40001  dihjatcclem1  40092  baerlem3lem1  40381  isdomn4  40835  pellfundex  41393  rmxypairf1o  41419  rmxycomplete  41425  rmxyneg  41428  rmxyadd  41429  rmxy1  41430  rmxy0  41431  jm2.22  41503  proot1mul  41710  deg1mhm  41718  stoweidlem7  44494  stoweidlem36  44523