Theorem syl3an3b 1408

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  fnunres2  6611  fresaunres1  6713  fvun2  6932  fvpr2g  7146  nnmsucr  8561  entrfil  9119  enpr2  9926  xrlttr  13091  iccdil  13443  icccntr  13445  hashgt23el  14386  absexpz  15267  nn0rppwr  16530  posglbdg  18379  f1omvdco3  19424  isdrngd  20742  isdrngdOLD  20744  unicld  23011  2ndcdisj2  23422  logrec  26727  cdj3lem3  32509  bnj563  34886  bnj1033  35111  lindsadd  37934  stoweidlem14  46442