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  6653  fresaunres1  6756  fvun2  6978  fvpr2g  7197  nnmsucr  8638  entrfil  9204  enpr2  10087  xrlttr  13273  iccdil  13625  icccntr  13627  hashgt23el  14573  absexpz  15478  nn0rppwr  16741  posglbdg  18593  f1omvdco3  19669  isdrngd  21028  isdrngdOLD  21030  unicld  23370  2ndcdisj2  23782  logrec  27097  cdj3lem3  33046  bnj563  35421  bnj1033  35646  mirimanoffr  36547  lindsadd  38630  stoweidlem14  47118