Theorem syl3an3b 1402

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

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

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 1086

This theorem is referenced by:  fnunres2  6668  fresaunres1  6770  fvun2  6989  fvpr2g  7200  nnmsucr  8646  entrfil  9213  enpr2  10027  xrlttr  13154  iccdil  13502  icccntr  13504  hashgt23el  14419  absexpz  15288  posglbdg  18410  f1omvdco3  19416  isdrngd  20669  isdrngdOLD  20671  unicld  22994  2ndcdisj2  23405  logrec  26740  cdj3lem3  32320  bnj563  34505  bnj1033  34731  lindsadd  37217  nn0rppwr  42028  stoweidlem14  45540