Theorem bj-imn3ani

Description: Duplication of bnj1224 . Three-fold version of imnani . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by BJ, 22-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-imn3ani.1	|- -. ( ph /\ ps /\ ch )
Assertion	bj-imn3ani	|- ( ( ph /\ ps ) -> -. ch )

Proof

Step	Hyp	Ref	Expression
1		bj-imn3ani.1	|- -. ( ph /\ ps /\ ch )
2		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
3	1 2	mtbi	|- -. ( ( ph /\ ps ) /\ ch )
4	3	imnani	|- ( ( ph /\ ps ) -> -. ch )