Theorem syl3an3b 1405

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 1087

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 1089

This theorem is referenced by:  fnunres2  6692  fresaunres1  6794  fvun2  7014  fvpr2g  7225  nnmsucr  8681  entrfil  9251  enpr2  10071  xrlttr  13202  iccdil  13550  icccntr  13552  hashgt23el  14473  absexpz  15354  nn0rppwr  16608  posglbdg  18485  f1omvdco3  19491  isdrngd  20787  isdrngdOLD  20789  unicld  23075  2ndcdisj2  23486  logrec  26824  cdj3lem3  32470  bnj563  34719  bnj1033  34945  lindsadd  37573  stoweidlem14  45935