Theorem syl3an3b 1432

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  fnunres2  6655  fresaunres1  6758  fvun2  6980  fvpr2g  7196  nnmsucr  8620  entrfil  9179  enpr2  10007  xrlttr  13183  iccdil  13535  icccntr  13537  hashgt23el  14481  absexpz  15382  nn0rppwr  16644  posglbdg  18494  f1omvdco3  19550  isdrngd  20905  isdrngdOLD  20907  unicld  23240  2ndcdisj2  23651  logrec  26965  cdj3lem3  32827  bnj563  35164  bnj1033  35389  lindsadd  38305  stoweidlem14  46769