Metamath Proof Explorer


Theorem ifpim1g

Description: Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020)

Ref Expression
Assertion ifpim1g if-φχθif-ψχθψφθχφψχθ

Proof

Step Hyp Ref Expression
1 ifpim123g if-φχθif-ψχθφ¬ψχχψφθχφψχθ¬ψφθθ
2 id χχ
3 2 olci φ¬ψχχ
4 3 biantrur ψφθχφ¬ψχχψφθχ
5 4 bicomi φ¬ψχχψφθχψφθχ
6 id θθ
7 6 olci ¬ψφθθ
8 7 biantru φψχθφψχθ¬ψφθθ
9 8 bicomi φψχθ¬ψφθθφψχθ
10 5 9 anbi12i φ¬ψχχψφθχφψχθ¬ψφθθψφθχφψχθ
11 1 10 bitri if-φχθif-ψχθψφθχφψχθ