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  6649  fresaunres1  6752  fvun2  6974  fvpr2g  7193  nnmsucr  8617  entrfil  9183  enpr2  10011  xrlttr  13195  iccdil  13547  icccntr  13549  hashgt23el  14493  absexpz  15396  nn0rppwr  16657  posglbdg  18507  f1omvdco3  19582  isdrngd  20937  isdrngdOLD  20939  unicld  23277  2ndcdisj2  23689  logrec  27008  cdj3lem3  32927  bnj563  35261  bnj1033  35486  lindsadd  38375  stoweidlem14  46850