Metamath Proof Explorer


Theorem simplbiim

Description: Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Wolf Lammen, 26-Mar-2022)

Ref Expression
Hypotheses simplbiim.1 φ ψ χ
simplbiim.2 χ θ
Assertion simplbiim φ θ

Proof

Step Hyp Ref Expression
1 simplbiim.1 φ ψ χ
2 simplbiim.2 χ θ
3 1 simprbi φ χ
4 3 2 syl φ θ