Theorem syl3an3b 1407

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 1165	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  6594  fresaunres1  6696  fvun2  6914  fvpr2g  7125  nnmsucr  8540  entrfil  9094  enpr2  9895  xrlttr  13039  iccdil  13390  icccntr  13392  hashgt23el  14331  absexpz  15212  nn0rppwr  16472  posglbdg  18319  f1omvdco3  19362  isdrngd  20681  isdrngdOLD  20683  unicld  22962  2ndcdisj2  23373  logrec  26701  cdj3lem3  32416  bnj563  34753  bnj1033  34979  lindsadd  37659  stoweidlem14  46058