Theorem bj-andnotim

Description: Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-andnotim	|- ( ( ( ph /\ -. ps ) -> ch ) <-> ( ( ph -> ps ) \/ ch ) )

Proof

Step	Hyp	Ref	Expression
1		imor	|- ( ( ( ph /\ -. ps ) -> ch ) <-> ( -. ( ph /\ -. ps ) \/ ch ) )
2		iman	|- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
3	2	biimpri	|- ( -. ( ph /\ -. ps ) -> ( ph -> ps ) )
4	3	orim1i	|- ( ( -. ( ph /\ -. ps ) \/ ch ) -> ( ( ph -> ps ) \/ ch ) )
5	1 4	sylbi	|- ( ( ( ph /\ -. ps ) -> ch ) -> ( ( ph -> ps ) \/ ch ) )
6		pm2.24	|- ( ps -> ( -. ps -> ch ) )
7	6	imim2i	|- ( ( ph -> ps ) -> ( ph -> ( -. ps -> ch ) ) )
8	7	impd	|- ( ( ph -> ps ) -> ( ( ph /\ -. ps ) -> ch ) )
9		ax-1	|- ( ch -> ( ( ph /\ -. ps ) -> ch ) )
10	8 9	jaoi	|- ( ( ( ph -> ps ) \/ ch ) -> ( ( ph /\ -. ps ) -> ch ) )
11	5 10	impbii	|- ( ( ( ph /\ -. ps ) -> ch ) <-> ( ( ph -> ps ) \/ ch ) )