Theorem syl23anc 1380

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 1375	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  8154  suppofss2d  8155  cnfcomlem  9620  ackbij1lem16  10156  div2subd  11981  symg2bas  19368  psgndiflemA  21581  evl1expd  22310  evls1maplmhm  22342  oftpos  22417  restopn2  23142  tsmsxp  24120  blcld  24470  cnllycmp  24923  dvlipcn  25961  tanregt0  26503  ostthlem1  27590  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbnd1lem1  27687  noinfbnd2  27695  ax5seglem6  29003  axcontlem4  29036  axcontlem7  29039  wwlksnextwrd  29965  drngidlhash  33494  rhmpreimaprmidl  33511  qsdrngilem  33554  rsprprmprmidlb  33583  rprmirredb  33592  dfufd2lem  33609  lindsunlem  33768  lactlmhm  33778  pnfneige0  34095  qqhval2  34126  esumcocn  34224  carsgmon  34458  bnj1125  35134  heiborlem8  38139  2atjm  39891  1cvrat  39922  lvolnlelln  40030  lvolnlelpln  40031  4atlem3  40042  lplncvrlvol  40062  dalem39  40157  cdleme4a  40685  cdleme15  40724  cdleme16c  40726  cdleme19b  40750  cdleme19e  40753  cdleme20d  40758  cdleme20g  40761  cdleme20j  40764  cdleme20k  40765  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme27cl  40812  cdlemefr27cl  40849  mpaaeu  43578