This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem syl2anbr

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999)

Ref Expression
Hypotheses syl2anbr.1 ⊢ ( 𝜓 ↔ 𝜑 )
syl2anbr.2 ⊢ ( 𝜒 ↔ 𝜏 )
syl2anbr.3 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion syl2anbr ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 syl2anbr.1 ⊢ ( 𝜓 ↔ 𝜑 )
2 syl2anbr.2 ⊢ ( 𝜒 ↔ 𝜏 )
3 syl2anbr.3 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4 1 3 sylanbr ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
5 2 4 sylan2br ⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )