Theorem syl3an3b 1432

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

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

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 1105

This theorem is referenced by:  fnunres2  6650  fresaunres1  6753  fvun2  6975  fvpr2g  7191  nnmsucr  8612  entrfil  9170  enpr2  9989  xrlttr  13166  iccdil  13518  icccntr  13520  hashgt23el  14463  absexpz  15358  nn0rppwr  16620  posglbdg  18470  f1omvdco3  19520  isdrngd  20850  isdrngdOLD  20852  unicld  23184  2ndcdisj2  23595  logrec  26909  cdj3lem3  32771  bnj563  35113  bnj1033  35338  lindsadd  38245  stoweidlem14  46711