Theorem syl3an3b 1428

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  fnunres2  6638  fresaunres1  6741  fvun2  6963  fvpr2g  7179  nnmsucr  8599  entrfil  9157  enpr2  9976  xrlttr  13153  iccdil  13505  icccntr  13507  hashgt23el  14449  absexpz  15344  nn0rppwr  16607  posglbdg  18457  f1omvdco3  19507  isdrngd  20835  isdrngdOLD  20837  unicld  23160  2ndcdisj2  23571  logrec  26882  cdj3lem3  32695  bnj563  35044  bnj1033  35269  lindsadd  38119  stoweidlem14  46587