Theorem syl23anc 1377

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl23anc.6	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl23anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl23anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1372	1 ⊢ (𝜑 → 𝜁)

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

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 1089

This theorem is referenced by:  suppofss1d  8140  suppofss2d  8141  cnfcomlem  9644  ackbij1lem16  10180  div2subd  11990  symg2bas  19188  psgndiflemA  21042  evl1expd  21748  oftpos  21838  restopn2  22565  tsmsxp  23543  blcld  23898  cnllycmp  24356  dvlipcn  25395  tanregt0  25932  ostthlem1  27012  nosupbnd1lem1  27093  nosupbnd2  27101  noinfbnd1lem1  27108  noinfbnd2  27116  ax5seglem6  27946  axcontlem4  27979  axcontlem7  27982  wwlksnextwrd  28905  rhmpreimaprmidl  32300  lindsunlem  32406  evls1maplmhm  32456  pnfneige0  32621  qqhval2  32652  esumcocn  32768  carsgmon  33003  bnj1125  33693  heiborlem8  36350  2atjm  37981  1cvrat  38012  lvolnlelln  38120  lvolnlelpln  38121  4atlem3  38132  lplncvrlvol  38152  dalem39  38247  cdleme4a  38775  cdleme15  38814  cdleme16c  38816  cdleme19b  38840  cdleme19e  38843  cdleme20d  38848  cdleme20g  38851  cdleme20j  38854  cdleme20k  38855  cdleme20l2  38857  cdleme20l  38858  cdleme20m  38859  cdleme22e  38880  cdleme22eALTN  38881  cdleme22f  38882  cdleme27cl  38902  cdlemefr27cl  38939  mpaaeu  41535