Theorem syl3an3b 1408

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 216	. 2 ⊢ (𝜑 → 𝜃)
3		syl3an3b.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl3an3 1166	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  fnunres2  6605  fresaunres1  6707  fvun2  6926  fvpr2g  7139  nnmsucr  8554  entrfil  9112  enpr2  9917  xrlttr  13082  iccdil  13434  icccntr  13436  hashgt23el  14377  absexpz  15258  nn0rppwr  16521  posglbdg  18370  f1omvdco3  19415  isdrngd  20733  isdrngdOLD  20735  unicld  23021  2ndcdisj2  23432  logrec  26740  cdj3lem3  32524  bnj563  34902  bnj1033  35127  lindsadd  37948  stoweidlem14  46460