syld3an1 - Metamath Proof Explorer

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

Theorem syld3an1 1408

Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

**Hypotheses**
Ref	Expression
syld3an1.1	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
syld3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

**Assertion**
Ref	Expression
syld3an1	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

**Proof of Theorem syld3an1**
Step	Hyp	Ref	Expression
1		syld3an1.1	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
2		simp2 1135	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1136	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1369	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ 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: f1dom2g 8990 f1domfi2 9210 entrfi 9218 entrfir 9219 domtrfil 9220 domtrfi 9221 domtrfir 9222 php3 9237 findcard3 9310 npncan 11512 nnpcan 11514 ppncan 11533 muldivdir 11938 subdivcomb1 11940 div2neg 11968 ltmuldiv 12118 opfi1uzind 14495 sgrp2nmndlem4 18880 zndvds 21483 wsuceq123 35410 atlrelat1 38793 cvlatcvr1 38813 dih11 40738 wessf1ornlem 44558 mullimc 45004 mullimcf 45011 icccncfext 45275 stoweidlem34 45422 stoweidlem49 45437 stoweidlem57 45445 sigarexp 46247 f1ocof1ob 46461 el0ldepsnzr 47535

	
		OSZAR »