Theorem syl23anc 1379

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 511	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl23anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	3, 4, 5, 6, 7	syl13anc 1374	1 ⊢ (𝜑 → 𝜁)

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

This theorem is referenced by:  suppofss1d  8140  suppofss2d  8141  cnfcomlem  9596  ackbij1lem16  10132  div2subd  11954  symg2bas  19307  psgndiflemA  21540  evl1expd  22261  evls1maplmhm  22293  oftpos  22368  restopn2  23093  tsmsxp  24071  blcld  24421  cnllycmp  24883  dvlipcn  25927  tanregt0  26476  ostthlem1  27566  nosupbnd1lem1  27648  nosupbnd2  27656  noinfbnd1lem1  27663  noinfbnd2  27671  ax5seglem6  28914  axcontlem4  28947  axcontlem7  28950  wwlksnextwrd  29877  drngidlhash  33406  rhmpreimaprmidl  33423  qsdrngilem  33466  rsprprmprmidlb  33495  rprmirredb  33504  dfufd2lem  33521  lindsunlem  33658  lactlmhm  33668  pnfneige0  33985  qqhval2  34016  esumcocn  34114  carsgmon  34348  bnj1125  35025  heiborlem8  37879  2atjm  39565  1cvrat  39596  lvolnlelln  39704  lvolnlelpln  39705  4atlem3  39716  lplncvrlvol  39736  dalem39  39831  cdleme4a  40359  cdleme15  40398  cdleme16c  40400  cdleme19b  40424  cdleme19e  40427  cdleme20d  40432  cdleme20g  40435  cdleme20j  40438  cdleme20k  40439  cdleme20l2  40441  cdleme20l  40442  cdleme20m  40443  cdleme22e  40464  cdleme22eALTN  40465  cdleme22f  40466  cdleme27cl  40486  cdlemefr27cl  40523  mpaaeu  43268