Theorem 3adant1l 1174

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant1l	⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant1l

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an1 1161	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:  ad5ant245  1359  cfsmolem  10294  axdc3lem4  10477  issubmnd  18721  mhmima  18777  rhmimasubrng  20503  maducoeval2  22555  cramerlem3  22604  restnlly  23399  efgh  26488  hasheuni  33704  matunitlindflem1  37089  pellex  42255  mendlmod  42617  disjf1o  44564  ssfiunibd  44691  mullimc  45004  mullimcf  45011  limclner  45039  limsupresxr  45154  liminfresxr  45155  sge0lefi  45786  isomenndlem  45918  hoicvr  45936  ovncvrrp  45952

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »