Theorem syl221anc 1409

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 521	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1404	1 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl222anc  1414  vtocldf  3525  f1oprswap  6899  dmdcand  12160  modmul12d  14106  modnegd  14107  modadd12d  14108  exprec  14284  rpexpmord  14349  splval2  14946  dvdsmodexp  16471  eulerthlem2  17000  fermltl  17002  odzdvds  17014  fnpr2o  17770  efgredleme  19999  efgredlemc  20001  blssps  24787  blss  24788  metequiv2  24873  met1stc  24884  met2ndci  24885  metdstri  25215  xlebnum  25330  caubl  25673  divcxp  27061  cxple2a  27073  cxplead  27095  cxplt2d  27100  cxple2d  27101  mulcxpd  27102  ang180  27188  wilthlem2  27442  lgsvalmod  27689  lgsmod  27696  lgsdir2lem4  27701  lgsdirprm  27704  lgsne0  27708  lgseisen  27752  conway  28211  ax5seglem9  29561  fzm1ne1  33466  xrsmulgzz  33659  linds2eq  34033  heiborlem8  39011  cdlemd4  41517  cdleme15a  41590  cdleme17b  41603  cdleme25a  41669  cdleme25c  41671  cdleme25dN  41672  cdleme26ee  41676  tendococl  42088  tendodi1  42100  tendodi2  42101  cdlemi  42136  tendocan  42140  cdlemk5a  42151  cdlemk5  42152  cdlemk10  42159  cdlemk5u  42177  cdlemkfid1N  42237  pellexlem6  44101  acongeq  44250  jm2.25  44266  stoweidlem42  47319  stoweidlem51  47328  ldepspr  49910