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  6656  fresaunres1  6756  fvun2  6976  fvpr2g  7188  nnmsucr  8642  entrfil  9204  enpr2  10021  xrlttr  13161  iccdil  13512  icccntr  13514  hashgt23el  14447  absexpz  15329  nn0rppwr  16585  posglbdg  18430  f1omvdco3  19435  isdrngd  20730  isdrngdOLD  20732  unicld  22989  2ndcdisj2  23400  logrec  26730  cdj3lem3  32424  bnj563  34779  bnj1033  35005  lindsadd  37642  stoweidlem14  46010