3adant2r - Metamath Proof Explorer

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

Theorem 3adant2r 1177

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
3adant2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

**Proof of Theorem 3adant2r**
Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1162	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Colors of variables: wff setvar class

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: ltdiv23 12136 lediv23 12137 divalglem8 16377 isdrngd 20657 isdrngdOLD 20659 deg1tm 26067 ax5seglem1 28752 ax5seglem2 28753 nvaddsub4 30480 nmoub2i 30597 cdleme21at 39801 cdleme42f 39953 trlcoabs2N 40195 tendoplcl2 40251 tendopltp 40253 cdlemk2 40305 cdlemk8 40311 cdlemk9 40312 cdlemk9bN 40313 cdleml8 40456 dihglblem3N 40768 dihglblem3aN 40769 fourierdlem42 45537 lincscm 47498 itsclc0yqsol 47837

	
		OSZAR »