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  6601  fresaunres1  6703  fvun2  6922  fvpr2g  7133  nnmsucr  8548  entrfil  9103  enpr2  9904  xrlttr  13043  iccdil  13394  icccntr  13396  hashgt23el  14335  absexpz  15216  nn0rppwr  16476  posglbdg  18323  f1omvdco3  19365  isdrngd  20684  isdrngdOLD  20686  unicld  22964  2ndcdisj2  23375  logrec  26703  cdj3lem3  32422  bnj563  34778  bnj1033  35004  lindsadd  37676  stoweidlem14  46139