3adant2l - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 3adant2l		Structured version Visualization version GIF version

Theorem 3adant2l 1175

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

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

**Assertion**
Ref	Expression
3adant2l	⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

**Proof of Theorem 3adant2l**
Step	Hyp	Ref	Expression
1		simpr 483	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1161	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084

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 395 df-3an 1086

This theorem is referenced by: axdc3lem4 10478 modexp 14236 lmmbr2 25231 ax5seglem1 28811 ax5seglem2 28812 nvaddsub4 30539 pl1cn 33687 athgt 39059 ltrncoelN 39746 ltrncoat 39747 trlcoabs 40324 tendoplcl2 40381 tendopltp 40383 dih1dimatlem0 40931 pellex 42397 fourierdlem42 45675

	
		OSZAR »