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  8146  suppofss2d  8147  cnfcomlem  9608  ackbij1lem16  10144  div2subd  11967  symg2bas  19322  psgndiflemA  21556  evl1expd  22289  evls1maplmhm  22321  oftpos  22396  restopn2  23121  tsmsxp  24099  blcld  24449  cnllycmp  24911  dvlipcn  25955  tanregt0  26504  ostthlem1  27594  nosupbnd1lem1  27676  nosupbnd2  27684  noinfbnd1lem1  27691  noinfbnd2  27699  ax5seglem6  29007  axcontlem4  29040  axcontlem7  29043  wwlksnextwrd  29970  drngidlhash  33515  rhmpreimaprmidl  33532  qsdrngilem  33575  rsprprmprmidlb  33604  rprmirredb  33613  dfufd2lem  33630  lindsunlem  33781  lactlmhm  33791  pnfneige0  34108  qqhval2  34139  esumcocn  34237  carsgmon  34471  bnj1125  35148  heiborlem8  38015  2atjm  39701  1cvrat  39732  lvolnlelln  39840  lvolnlelpln  39841  4atlem3  39852  lplncvrlvol  39872  dalem39  39967  cdleme4a  40495  cdleme15  40534  cdleme16c  40536  cdleme19b  40560  cdleme19e  40563  cdleme20d  40568  cdleme20g  40571  cdleme20j  40574  cdleme20k  40575  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme22e  40600  cdleme22eALTN  40601  cdleme22f  40602  cdleme27cl  40622  cdlemefr27cl  40659  mpaaeu  43388