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  3522  f1oprswap  6868  dmdcand  12115  modmul12d  14061  modnegd  14062  modadd12d  14063  exprec  14239  rpexpmord  14304  splval2  14899  dvdsmodexp  16423  eulerthlem2  16952  fermltl  16954  odzdvds  16966  fnpr2o  17722  efgredleme  19950  efgredlemc  19952  blssps  24736  blss  24737  metequiv2  24822  met1stc  24833  met2ndci  24834  metdstri  25164  xlebnum  25279  caubl  25622  divcxp  27008  cxple2a  27020  cxplead  27042  cxplt2d  27047  cxple2d  27048  mulcxpd  27049  ang180  27135  wilthlem2  27389  lgsvalmod  27636  lgsmod  27643  lgsdir2lem4  27648  lgsdirprm  27651  lgsne0  27655  lgseisen  27699  conway  28158  ax5seglem9  29508  fzm1ne1  33373  xrsmulgzz  33563  linds2eq  33929  heiborlem8  38732  cdlemd4  41238  cdleme15a  41311  cdleme17b  41324  cdleme25a  41390  cdleme25c  41392  cdleme25dN  41393  cdleme26ee  41397  tendococl  41809  tendodi1  41821  tendodi2  41822  cdlemi  41857  tendocan  41861  cdlemk5a  41872  cdlemk5  41873  cdlemk10  41880  cdlemk5u  41898  cdlemkfid1N  41958  pellexlem6  43820  acongeq  43969  jm2.25  43985  stoweidlem42  47021  stoweidlem51  47030  ldepspr  49554