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  6871  dmdcand  12126  modmul12d  14072  modnegd  14073  modadd12d  14074  exprec  14250  rpexpmord  14315  splval2  14911  dvdsmodexp  16436  eulerthlem2  16965  fermltl  16967  odzdvds  16979  fnpr2o  17735  efgredleme  19963  efgredlemc  19965  blssps  24749  blss  24750  metequiv2  24835  met1stc  24846  met2ndci  24847  metdstri  25177  xlebnum  25292  caubl  25635  divcxp  27021  cxple2a  27033  cxplead  27055  cxplt2d  27060  cxple2d  27061  mulcxpd  27062  ang180  27148  wilthlem2  27402  lgsvalmod  27649  lgsmod  27656  lgsdir2lem4  27661  lgsdirprm  27664  lgsne0  27668  lgseisen  27712  conway  28171  ax5seglem9  29521  fzm1ne1  33427  xrsmulgzz  33617  linds2eq  33983  heiborlem8  38846  cdlemd4  41352  cdleme15a  41425  cdleme17b  41438  cdleme25a  41504  cdleme25c  41506  cdleme25dN  41507  cdleme26ee  41511  tendococl  41923  tendodi1  41935  tendodi2  41936  cdlemi  41971  tendocan  41975  cdlemk5a  41986  cdlemk5  41987  cdlemk10  41994  cdlemk5u  42012  cdlemkfid1N  42072  pellexlem6  43935  acongeq  44084  jm2.25  44100  stoweidlem42  47146  stoweidlem51  47155  ldepspr  49679