Theorem syl221anc 1382

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  syl222anc  1387  vtocldf  3542  f1oprswap  6878  dmdcand  12019  modmul12d  13890  modnegd  13891  modadd12d  13892  exprec  14069  rpexpmord  14133  splval2  14707  dvdsmodexp  16205  eulerthlem2  16715  fermltl  16717  odzdvds  16728  fnpr2o  17503  efgredleme  19611  efgredlemc  19613  blssps  23930  blss  23931  metequiv2  24019  met1stc  24030  met2ndci  24031  metdstri  24367  xlebnum  24481  caubl  24825  divcxp  26195  cxple2a  26207  cxplead  26229  cxplt2d  26234  cxple2d  26235  mulcxpd  26236  ang180  26319  wilthlem2  26573  lgsvalmod  26819  lgsmod  26826  lgsdir2lem4  26831  lgsdirprm  26834  lgsne0  26838  lgseisen  26882  conway  27300  ax5seglem9  28195  fzm1ne1  32000  xrsmulgzz  32179  linds2eq  32497  heiborlem8  36686  cdlemd4  39072  cdleme15a  39145  cdleme17b  39158  cdleme25a  39224  cdleme25c  39226  cdleme25dN  39227  cdleme26ee  39231  tendococl  39643  tendodi1  39655  tendodi2  39656  cdlemi  39691  tendocan  39695  cdlemk5a  39706  cdlemk5  39707  cdlemk10  39714  cdlemk5u  39732  cdlemkfid1N  39792  pellexlem6  41572  acongeq  41722  jm2.25  41738  stoweidlem42  44758  stoweidlem51  44767  ldepspr  47154