Theorem syl221anc 1408

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 1403	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  1413  vtocldf  3521  f1oprswap  6863  dmdcand  12044  modmul12d  13989  modnegd  13990  modadd12d  13991  exprec  14167  rpexpmord  14232  splval2  14826  dvdsmodexp  16350  eulerthlem2  16873  fermltl  16875  odzdvds  16887  fnpr2o  17643  efgredleme  19870  efgredlemc  19872  blssps  24650  blss  24651  metequiv2  24736  met1stc  24747  met2ndci  24748  metdstri  25078  xlebnum  25193  caubl  25536  divcxp  26924  cxple2a  26936  cxplead  26958  cxplt2d  26963  cxple2d  26964  mulcxpd  26965  ang180  27051  wilthlem2  27305  lgsvalmod  27552  lgsmod  27559  lgsdir2lem4  27564  lgsdirprm  27567  lgsne0  27571  lgseisen  27615  conway  28044  ax5seglem9  29394  fzm1ne1  33259  xrsmulgzz  33449  linds2eq  33814  heiborlem8  38568  cdlemd4  41074  cdleme15a  41147  cdleme17b  41160  cdleme25a  41226  cdleme25c  41228  cdleme25dN  41229  cdleme26ee  41233  tendococl  41645  tendodi1  41657  tendodi2  41658  cdlemi  41693  tendocan  41697  cdlemk5a  41708  cdlemk5  41709  cdlemk10  41716  cdlemk5u  41734  cdlemkfid1N  41794  pellexlem6  43675  acongeq  43824  jm2.25  43840  stoweidlem42  46870  stoweidlem51  46879  ldepspr  49403