Theorem syl3an3b 1403

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  fnunres2  6661  fresaunres1  6763  fvun2  6982  fvpr2g  7190  nnmsucr  8627  entrfil  9190  enpr2  9999  xrlttr  13123  iccdil  13471  icccntr  13473  hashgt23el  14388  absexpz  15256  posglbdg  18372  f1omvdco3  19358  isdrngd  20533  isdrngdOLD  20535  unicld  22770  2ndcdisj2  23181  logrec  26504  cdj3lem3  31958  bnj563  34052  bnj1033  34278  lindsadd  36784  nn0rppwr  41526  stoweidlem14  45028