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  3515  f1oprswap  6807  dmdcand  11923  modmul12d  13829  modnegd  13830  modadd12d  13831  exprec  14007  rpexpmord  14072  splval2  14661  dvdsmodexp  16168  eulerthlem2  16690  fermltl  16692  odzdvds  16704  fnpr2o  17458  efgredleme  19653  efgredlemc  19655  blssps  24337  blss  24338  metequiv2  24423  met1stc  24434  met2ndci  24435  metdstri  24765  xlebnum  24889  caubl  25233  divcxp  26621  cxple2a  26633  cxplead  26655  cxplt2d  26660  cxple2d  26661  mulcxpd  26662  ang180  26749  wilthlem2  27004  lgsvalmod  27252  lgsmod  27259  lgsdir2lem4  27264  lgsdirprm  27267  lgsne0  27271  lgseisen  27315  conway  27738  ax5seglem9  28913  fzm1ne1  32766  xrsmulgzz  32985  linds2eq  33341  heiborlem8  37857  cdlemd4  40239  cdleme15a  40312  cdleme17b  40325  cdleme25a  40391  cdleme25c  40393  cdleme25dN  40394  cdleme26ee  40398  tendococl  40810  tendodi1  40822  tendodi2  40823  cdlemi  40858  tendocan  40862  cdlemk5a  40873  cdlemk5  40874  cdlemk10  40881  cdlemk5u  40899  cdlemkfid1N  40959  pellexlem6  42866  acongeq  43015  jm2.25  43031  stoweidlem42  46079  stoweidlem51  46088  ldepspr  48504