Theorem syl3an3b 1413

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  fnunres2  6605  fresaunres1  6707  fvun2  6926  fvpr2g  7142  nnmsucr  8558  entrfil  9116  enpr2  9924  xrlttr  13089  iccdil  13441  icccntr  13443  hashgt23el  14384  absexpz  15265  nn0rppwr  16528  posglbdg  18377  f1omvdco3  19422  isdrngd  20744  isdrngdOLD  20746  unicld  23036  2ndcdisj2  23447  logrec  26752  cdj3lem3  32534  bnj563  34933  bnj1033  35158  lindsadd  37987  stoweidlem14  46464