Theorem syl3an3b 1406

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  fnunres2  6663  fresaunres1  6765  fvun2  6984  fvpr2g  7189  nnmsucr  8625  entrfil  9188  enpr2  9997  xrlttr  13119  iccdil  13467  icccntr  13469  hashgt23el  14384  absexpz  15252  posglbdg  18368  f1omvdco3  19317  isdrngd  20390  isdrngdOLD  20392  unicld  22550  2ndcdisj2  22961  logrec  26268  cdj3lem3  31691  bnj563  33754  bnj1033  33980  lindsadd  36481  nn0rppwr  41224  stoweidlem14  44730