Metamath Proof Explorer


Theorem bian1d

Description: Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017)

Ref Expression
Hypothesis bian1d.1 φψχθ
Assertion bian1d φχψχθ

Proof

Step Hyp Ref Expression
1 bian1d.1 φψχθ
2 1 biimpd φψχθ
3 2 adantld φχψχθ
4 simpl χθχ
5 4 a1i φχθχ
6 1 biimprd φχθψ
7 5 6 jcad φχθχψ
8 3 7 impbid φχψχθ