Theorem syl23anc 1445

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  suppofss1d  7616  suppofss2d  7617  cnfcomlem  8895  ackbij1lem16  9394  div2subd  11203  symg2bas  18205  evl1expd  20109  psgndiflemA  20347  oftpos  20667  restopn2  21393  tsmsxp  22370  blcld  22722  metustexhalf  22773  cnllycmp  23167  dvlipcn  24198  tanregt0  24727  ostthlem1  25772  ax5seglem6  26287  axcontlem4  26320  axcontlem7  26323  wwlksnextwrd  27265  wwlksnextwrdOLD  27270  lindsunlem  30442  pnfneige0  30599  qqhval2  30628  esumcocn  30744  carsgmon  30978  bnj1125  31663  nosupbnd1lem1  32447  nosupbnd2  32455  heiborlem8  34246  2atjm  35604  1cvrat  35635  lvolnlelln  35743  lvolnlelpln  35744  4atlem3  35755  lplncvrlvol  35775  dalem39  35870  cdleme4a  36398  cdleme15  36437  cdleme16c  36439  cdleme19b  36463  cdleme19e  36466  cdleme20d  36471  cdleme20g  36474  cdleme20j  36477  cdleme20k  36478  cdleme20l2  36480  cdleme20l  36481  cdleme20m  36482  cdleme22e  36503  cdleme22eALTN  36504  cdleme22f  36505  cdleme27cl  36525  cdlemefr27cl  36562  mpaaeu  38689