Metamath Proof Explorer


Theorem wl-ifp4impr

Description: If one case of an if- condition is a consequence of the other, the expression in dfifp4 can be shortened. (Contributed by Wolf Lammen, 18-Jun-2024)

Ref Expression
Assertion wl-ifp4impr χ ψ if- φ ψ χ φ χ ψ

Proof

Step Hyp Ref Expression
1 wl-ifpimpr χ ψ if- φ ψ χ φ ψ χ
2 pm4.71 χ ψ χ χ ψ
3 2 biimpi χ ψ χ χ ψ
4 3 orbi2d χ ψ φ ψ χ φ ψ χ ψ
5 andir φ χ ψ φ ψ χ ψ
6 4 5 bitr4di χ ψ φ ψ χ φ χ ψ
7 1 6 bitrd χ ψ if- φ ψ χ φ χ ψ