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 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  6680  fresaunres1  6780  fvun2  7000  fvpr2g  7212  nnmsucr  8664  entrfil  9226  enpr2  10043  xrlttr  13183  iccdil  13531  icccntr  13533  hashgt23el  14464  absexpz  15345  nn0rppwr  16599  posglbdg  18461  f1omvdco3  19468  isdrngd  20766  isdrngdOLD  20768  unicld  23055  2ndcdisj2  23466  logrec  26807  cdj3lem3  32458  bnj563  34758  bnj1033  34984  lindsadd  37621  stoweidlem14  46034