Theorem syl3an3b 1433

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  6677  fresaunres1  6780  fvun2  7003  fvpr2g  7222  nnmsucr  8665  entrfil  9231  enpr2  10113  xrlttr  13299  iccdil  13651  icccntr  13653  hashgt23el  14599  absexpz  15504  nn0rppwr  16767  posglbdg  18619  f1omvdco3  19696  isdrngd  21055  isdrngdOLD  21057  unicld  23397  2ndcdisj2  23809  logrec  27124  cdj3lem3  33073  bnj563  35457  bnj1033  35682  mirimanoffr  36640  lindsadd  38741  stoweidlem14  47239