Theorem syld3an1 1412

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 1137	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1138	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  f1dom2g  8944  f1domfi2  9152  entrfi  9160  entrfir  9161  domtrfil  9162  domtrfi  9163  domtrfir  9164  php3  9179  findcard3  9236  npncan  11450  nnpcan  11452  ppncan  11471  muldivdir  11882  subdivcomb1  11884  div2neg  11912  ltmuldiv  12063  opfi1uzind  14483  sgrp2nmndlem4  18862  zndvds  21466  wsuceq123  35809  atlrelat1  39321  cvlatcvr1  39341  dih11  41266  wessf1ornlem  45186  mullimc  45621  mullimcf  45628  icccncfext  45892  stoweidlem34  46039  stoweidlem49  46054  stoweidlem57  46062  sigarexp  46864  f1ocof1ob  47086  el0ldepsnzr  48460