Theorem syl221anc 1380

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl222anc  1385  vtocldf  3493  f1oprswap  6760  dmdcand  11780  modmul12d  13645  modnegd  13646  modadd12d  13647  exprec  13824  rpexpmord  13886  splval2  14470  dvdsmodexp  15971  eulerthlem2  16483  fermltl  16485  odzdvds  16496  fnpr2o  17268  efgredleme  19349  efgredlemc  19351  blssps  23577  blss  23578  metequiv2  23666  met1stc  23677  met2ndci  23678  metdstri  24014  xlebnum  24128  caubl  24472  divcxp  25842  cxple2a  25854  cxplead  25876  cxplt2d  25881  cxple2d  25882  mulcxpd  25883  ang180  25964  wilthlem2  26218  lgsvalmod  26464  lgsmod  26471  lgsdir2lem4  26476  lgsdirprm  26479  lgsne0  26483  lgseisen  26527  ax5seglem9  27305  fzm1ne1  31110  xrsmulgzz  31287  linds2eq  31575  conway  33993  heiborlem8  35976  cdlemd4  38215  cdleme15a  38288  cdleme17b  38301  cdleme25a  38367  cdleme25c  38369  cdleme25dN  38370  cdleme26ee  38374  tendococl  38786  tendodi1  38798  tendodi2  38799  cdlemi  38834  tendocan  38838  cdlemk5a  38849  cdlemk5  38850  cdlemk10  38857  cdlemk5u  38875  cdlemkfid1N  38935  pellexlem6  40656  acongeq  40805  jm2.25  40821  stoweidlem42  43583  stoweidlem51  43592  ldepspr  45814