Theorem ifpim2

Description: Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifpim2	|- ( ( ph -> ps ) <-> if- ( ps , T. , -. ph ) )

Proof

Step	Hyp	Ref	Expression
1		tru	|- T.
2	1	olci	|- ( -. ps \/ T. )
3	2	biantrur	|- ( ( ps \/ -. ph ) <-> ( ( -. ps \/ T. ) /\ ( ps \/ -. ph ) ) )
4		imor	|- ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
5		orcom	|- ( ( -. ph \/ ps ) <-> ( ps \/ -. ph ) )
6	4 5	bitri	|- ( ( ph -> ps ) <-> ( ps \/ -. ph ) )
7		dfifp4	|- ( if- ( ps , T. , -. ph ) <-> ( ( -. ps \/ T. ) /\ ( ps \/ -. ph ) ) )
8	3 6 7	3bitr4i	|- ( ( ph -> ps ) <-> if- ( ps , T. , -. ph ) )