Theorem syl221anc 1374

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 1369	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  syl222anc  1379  vtocldf  3498  f1oprswap  6526  dmdcand  11293  modmul12d  13143  modnegd  13144  modadd12d  13145  exprec  13320  rpexpmord  13382  splval2  13955  dvdsmodexp  15448  eulerthlem2  15948  fermltl  15950  odzdvds  15961  fnpr2o  16659  efgredleme  18596  efgredlemc  18598  blssps  22717  blss  22718  metequiv2  22803  met1stc  22814  met2ndci  22815  metdstri  23142  xlebnum  23252  caubl  23594  divcxp  24951  cxple2a  24963  cxplead  24985  cxplt2d  24990  cxple2d  24991  mulcxpd  24992  ang180  25073  wilthlem2  25328  lgsvalmod  25574  lgsmod  25581  lgsdir2lem4  25586  lgsdirprm  25589  lgsne0  25593  lgseisen  25637  ax5seglem9  26406  xrsmulgzz  30339  linds2eq  30587  conway  32873  etasslt  32883  heiborlem8  34628  cdlemd4  36868  cdleme15a  36941  cdleme17b  36954  cdleme25a  37020  cdleme25c  37022  cdleme25dN  37023  cdleme26ee  37027  tendococl  37439  tendodi1  37451  tendodi2  37452  cdlemi  37487  tendocan  37491  cdlemk5a  37502  cdlemk5  37503  cdlemk10  37510  cdlemk5u  37528  cdlemkfid1N  37588  pellexlem6  38916  acongeq  39065  jm2.25  39081  stoweidlem42  41869  stoweidlem51  41878  ldepspr  44008