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  6599  fresaunres1  6701  fvun2  6919  fvpr2g  7131  nnmsucr  8550  entrfil  9109  enpr2  9917  xrlttr  13060  iccdil  13411  icccntr  13413  hashgt23el  14349  absexpz  15230  nn0rppwr  16490  posglbdg  18337  f1omvdco3  19346  isdrngd  20668  isdrngdOLD  20670  unicld  22949  2ndcdisj2  23360  logrec  26689  cdj3lem3  32400  bnj563  34712  bnj1033  34938  lindsadd  37595  stoweidlem14  45999