ifpim1g

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

		Ref	Expression
	Assertion	ifpim1g	$⊢ (if- (φ, χ, θ) \to if- (ψ, χ, θ)) \leftrightarrow (((ψ \to φ) \lor (θ \to χ)) \land ((φ \to ψ) \lor (χ \to θ)))$

Step	Hyp	Ref	Expression
1		ifpim123g	$⊢ (if- (φ, χ, θ) \to if- (ψ, χ, θ)) \leftrightarrow ((((φ \to \neg ψ) \lor (χ \to χ)) \land ((ψ \to φ) \lor (θ \to χ))) \land (((φ \to ψ) \lor (χ \to θ)) \land ((\neg ψ \to φ) \lor (θ \to θ))))$
2		id	$⊢ χ \to χ$
3	2	olci	$⊢ ((φ \to \neg ψ) \lor (χ \to χ))$
4	3	biantrur	$⊢ ((ψ \to φ) \lor (θ \to χ)) \leftrightarrow (((φ \to \neg ψ) \lor (χ \to χ)) \land ((ψ \to φ) \lor (θ \to χ)))$
5	4	bicomi	$⊢ (((φ \to \neg ψ) \lor (χ \to χ)) \land ((ψ \to φ) \lor (θ \to χ))) \leftrightarrow ((ψ \to φ) \lor (θ \to χ))$
6		id	$⊢ θ \to θ$
7	6	olci	$⊢ ((\neg ψ \to φ) \lor (θ \to θ))$
8	7	biantru	$⊢ ((φ \to ψ) \lor (χ \to θ)) \leftrightarrow (((φ \to ψ) \lor (χ \to θ)) \land ((\neg ψ \to φ) \lor (θ \to θ)))$
9	8	bicomi	$⊢ (((φ \to ψ) \lor (χ \to θ)) \land ((\neg ψ \to φ) \lor (θ \to θ))) \leftrightarrow ((φ \to ψ) \lor (χ \to θ))$
10	5 9	anbi12i	$⊢ ((((φ \to \neg ψ) \lor (χ \to χ)) \land ((ψ \to φ) \lor (θ \to χ))) \land (((φ \to ψ) \lor (χ \to θ)) \land ((\neg ψ \to φ) \lor (θ \to θ)))) \leftrightarrow (((ψ \to φ) \lor (θ \to χ)) \land ((φ \to ψ) \lor (χ \to θ)))$
11	1 10	bitri	$⊢ (if- (φ, χ, θ) \to if- (ψ, χ, θ)) \leftrightarrow (((ψ \to φ) \lor (θ \to χ)) \land ((φ \to ψ) \lor (χ \to θ)))$

Metamath Proof Explorer