Theorem syl23anc 1375

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  suppofss1d  7991  suppofss2d  7992  cnfcomlem  9387  ackbij1lem16  9922  div2subd  11731  symg2bas  18915  psgndiflemA  20718  evl1expd  21421  oftpos  21509  restopn2  22236  tsmsxp  23214  blcld  23567  cnllycmp  24025  dvlipcn  25063  tanregt0  25600  ostthlem1  26680  ax5seglem6  27205  axcontlem4  27238  axcontlem7  27241  wwlksnextwrd  28163  rhmpreimaprmidl  31529  lindsunlem  31607  pnfneige0  31803  qqhval2  31832  esumcocn  31948  carsgmon  32181  bnj1125  32872  nosupbnd1lem1  33838  nosupbnd2  33846  noinfbnd1lem1  33853  noinfbnd2  33861  heiborlem8  35903  2atjm  37386  1cvrat  37417  lvolnlelln  37525  lvolnlelpln  37526  4atlem3  37537  lplncvrlvol  37557  dalem39  37652  cdleme4a  38180  cdleme15  38219  cdleme16c  38221  cdleme19b  38245  cdleme19e  38248  cdleme20d  38253  cdleme20g  38256  cdleme20j  38259  cdleme20k  38260  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme27cl  38307  cdlemefr27cl  38344  mpaaeu  40891