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  6613  fresaunres1  6715  fvun2  6934  fvpr2g  7147  nnmsucr  8563  entrfil  9121  enpr2  9926  xrlttr  13066  iccdil  13418  icccntr  13420  hashgt23el  14359  absexpz  15240  nn0rppwr  16500  posglbdg  18348  f1omvdco3  19390  isdrngd  20710  isdrngdOLD  20712  unicld  23002  2ndcdisj2  23413  logrec  26741  cdj3lem3  32525  bnj563  34919  bnj1033  35144  lindsadd  37861  stoweidlem14  46369