Theorem syl221anc 1384

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

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

This theorem is referenced by:  syl222anc  1389  vtocldf  3506  f1oprswap  6819  dmdcand  11951  modmul12d  13878  modnegd  13879  modadd12d  13880  exprec  14056  rpexpmord  14121  splval2  14710  dvdsmodexp  16220  eulerthlem2  16743  fermltl  16745  odzdvds  16757  fnpr2o  17512  efgredleme  19709  efgredlemc  19711  blssps  24399  blss  24400  metequiv2  24485  met1stc  24496  met2ndci  24497  metdstri  24827  xlebnum  24942  caubl  25285  divcxp  26664  cxple2a  26676  cxplead  26698  cxplt2d  26703  cxple2d  26704  mulcxpd  26705  ang180  26791  wilthlem2  27046  lgsvalmod  27293  lgsmod  27300  lgsdir2lem4  27305  lgsdirprm  27308  lgsne0  27312  lgseisen  27356  conway  27785  ax5seglem9  29020  fzm1ne1  32876  xrsmulgzz  33084  linds2eq  33456  heiborlem8  38153  cdlemd4  40661  cdleme15a  40734  cdleme17b  40747  cdleme25a  40813  cdleme25c  40815  cdleme25dN  40816  cdleme26ee  40820  tendococl  41232  tendodi1  41244  tendodi2  41245  cdlemi  41280  tendocan  41284  cdlemk5a  41295  cdlemk5  41296  cdlemk10  41303  cdlemk5u  41321  cdlemkfid1N  41381  pellexlem6  43280  acongeq  43429  jm2.25  43445  stoweidlem42  46488  stoweidlem51  46497  ldepspr  48961