Theorem syl221anc 1383

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl221anc.6	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl221anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 511	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1378	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:  syl222anc  1388  vtocldf  3529  f1oprswap  6847  dmdcand  11994  modmul12d  13897  modnegd  13898  modadd12d  13899  exprec  14075  rpexpmord  14140  splval2  14729  dvdsmodexp  16237  eulerthlem2  16759  fermltl  16761  odzdvds  16773  fnpr2o  17527  efgredleme  19680  efgredlemc  19682  blssps  24319  blss  24320  metequiv2  24405  met1stc  24416  met2ndci  24417  metdstri  24747  xlebnum  24871  caubl  25215  divcxp  26603  cxple2a  26615  cxplead  26637  cxplt2d  26642  cxple2d  26643  mulcxpd  26644  ang180  26731  wilthlem2  26986  lgsvalmod  27234  lgsmod  27241  lgsdir2lem4  27246  lgsdirprm  27249  lgsne0  27253  lgseisen  27297  conway  27718  ax5seglem9  28871  fzm1ne1  32718  xrsmulgzz  32954  linds2eq  33359  heiborlem8  37819  cdlemd4  40202  cdleme15a  40275  cdleme17b  40288  cdleme25a  40354  cdleme25c  40356  cdleme25dN  40357  cdleme26ee  40361  tendococl  40773  tendodi1  40785  tendodi2  40786  cdlemi  40821  tendocan  40825  cdlemk5a  40836  cdlemk5  40837  cdlemk10  40844  cdlemk5u  40862  cdlemkfid1N  40922  pellexlem6  42829  acongeq  42979  jm2.25  42995  stoweidlem42  46047  stoweidlem51  46056  ldepspr  48466