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

This theorem is referenced by:  suppofss1d  8229  suppofss2d  8230  cnfcomlem  9739  ackbij1lem16  10274  div2subd  12093  symg2bas  19410  psgndiflemA  21619  evl1expd  22349  evls1maplmhm  22381  oftpos  22458  restopn2  23185  tsmsxp  24163  blcld  24518  cnllycmp  24988  dvlipcn  26033  tanregt0  26581  ostthlem1  27671  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbnd1lem1  27768  noinfbnd2  27776  ax5seglem6  28949  axcontlem4  28982  axcontlem7  28985  wwlksnextwrd  29917  drngidlhash  33462  rhmpreimaprmidl  33479  qsdrngilem  33522  rsprprmprmidlb  33551  rprmirredb  33560  dfufd2lem  33577  lindsunlem  33675  lactlmhm  33685  pnfneige0  33950  qqhval2  33983  esumcocn  34081  carsgmon  34316  bnj1125  35006  heiborlem8  37825  2atjm  39447  1cvrat  39478  lvolnlelln  39586  lvolnlelpln  39587  4atlem3  39598  lplncvrlvol  39618  dalem39  39713  cdleme4a  40241  cdleme15  40280  cdleme16c  40282  cdleme19b  40306  cdleme19e  40309  cdleme20d  40314  cdleme20g  40317  cdleme20j  40320  cdleme20k  40321  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme27cl  40368  cdlemefr27cl  40405  mpaaeu  43162