Theorem syl3an3b 1432

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3b.1	⊢ (𝜑 ↔ 𝜃)
syl3an3b.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3b	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3b

Step	Hyp	Ref	Expression
1		syl3an3b.1	. . 3 ⊢ (𝜑 ↔ 𝜃)
2	1	biimpi 219	. 2 ⊢ (𝜑 → 𝜃)
3		syl3an3b.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl3an3 1183	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fnunres2  6644  fresaunres1  6747  fvun2  6969  fvpr2g  7188  nnmsucr  8618  entrfil  9184  enpr2  10064  xrlttr  13250  iccdil  13602  icccntr  13604  hashgt23el  14549  absexpz  15452  nn0rppwr  16715  posglbdg  18567  f1omvdco3  19643  isdrngd  21002  isdrngdOLD  21004  unicld  23344  2ndcdisj2  23756  logrec  27073  cdj3lem3  33022  bnj563  35357  bnj1033  35582  lindsadd  38504  stoweidlem14  46968