Theorem syl3an3b 1404

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 1164	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  6682  fresaunres1  6782  fvun2  7001  fvpr2g  7211  nnmsucr  8662  entrfil  9223  enpr2  10040  xrlttr  13179  iccdil  13527  icccntr  13529  hashgt23el  14460  absexpz  15341  nn0rppwr  16595  posglbdg  18473  f1omvdco3  19482  isdrngd  20782  isdrngdOLD  20784  unicld  23070  2ndcdisj2  23481  logrec  26821  cdj3lem3  32467  bnj563  34736  bnj1033  34962  lindsadd  37600  stoweidlem14  45970