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  3539  f1oprswap  6862  dmdcand  12046  modmul12d  13943  modnegd  13944  modadd12d  13945  exprec  14121  rpexpmord  14186  splval2  14775  dvdsmodexp  16280  eulerthlem2  16801  fermltl  16803  odzdvds  16815  fnpr2o  17571  efgredleme  19724  efgredlemc  19726  blssps  24363  blss  24364  metequiv2  24449  met1stc  24460  met2ndci  24461  metdstri  24791  xlebnum  24915  caubl  25260  divcxp  26648  cxple2a  26660  cxplead  26682  cxplt2d  26687  cxple2d  26688  mulcxpd  26689  ang180  26776  wilthlem2  27031  lgsvalmod  27279  lgsmod  27286  lgsdir2lem4  27291  lgsdirprm  27294  lgsne0  27298  lgseisen  27342  conway  27763  ax5seglem9  28916  fzm1ne1  32765  xrsmulgzz  33001  linds2eq  33396  heiborlem8  37842  cdlemd4  40220  cdleme15a  40293  cdleme17b  40306  cdleme25a  40372  cdleme25c  40374  cdleme25dN  40375  cdleme26ee  40379  tendococl  40791  tendodi1  40803  tendodi2  40804  cdlemi  40839  tendocan  40843  cdlemk5a  40854  cdlemk5  40855  cdlemk10  40862  cdlemk5u  40880  cdlemkfid1N  40940  pellexlem6  42857  acongeq  43007  jm2.25  43023  stoweidlem42  46071  stoweidlem51  46080  ldepspr  48449