Theorem otthne

Description: Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypotheses	otthne.1	|- A e. _V
	otthne.2	|- B e. _V
	otthne.3	|- C e. _V
Assertion	otthne	|- ( <. <. A , B >. , C >. =/= <. <. D , E >. , F >. <-> ( A =/= D \/ B =/= E \/ C =/= F ) )

Proof

Step	Hyp	Ref	Expression
1		otthne.1	|- A e. _V
2		otthne.2	|- B e. _V
3		otthne.3	|- C e. _V
4	1 2	opthne	|- ( <. A , B >. =/= <. D , E >. <-> ( A =/= D \/ B =/= E ) )
5	4	orbi1i	|- ( ( <. A , B >. =/= <. D , E >. \/ C =/= F ) <-> ( ( A =/= D \/ B =/= E ) \/ C =/= F ) )
6		opex	|- <. A , B >. e. _V
7	6 3	opthne	|- ( <. <. A , B >. , C >. =/= <. <. D , E >. , F >. <-> ( <. A , B >. =/= <. D , E >. \/ C =/= F ) )
8		df-3or	|- ( ( A =/= D \/ B =/= E \/ C =/= F ) <-> ( ( A =/= D \/ B =/= E ) \/ C =/= F ) )
9	5 7 8	3bitr4i	|- ( <. <. A , B >. , C >. =/= <. <. D , E >. , F >. <-> ( A =/= D \/ B =/= E \/ C =/= F ) )