Theorem syl3an3b 1407

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 1165	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  fnunres2  6605  fresaunres1  6707  fvun2  6926  fvpr2g  7137  nnmsucr  8553  entrfil  9109  enpr2  9914  xrlttr  13054  iccdil  13406  icccntr  13408  hashgt23el  14347  absexpz  15228  nn0rppwr  16488  posglbdg  18336  f1omvdco3  19378  isdrngd  20698  isdrngdOLD  20700  unicld  22990  2ndcdisj2  23401  logrec  26729  cdj3lem3  32513  bnj563  34899  bnj1033  35125  lindsadd  37814  stoweidlem14  46258