Theorem syl3an3b 1423

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  fnunres2  6628  fresaunres1  6731  fvun2  6953  fvpr2g  7169  nnmsucr  8588  entrfil  9146  enpr2  9953  xrlttr  13135  iccdil  13487  icccntr  13489  hashgt23el  14430  absexpz  15322  nn0rppwr  16585  posglbdg  18435  f1omvdco3  19479  isdrngd  20801  isdrngdOLD  20803  unicld  23093  2ndcdisj2  23504  logrec  26815  cdj3lem3  32597  bnj563  34999  bnj1033  35224  lindsadd  38072  stoweidlem14  46548