ifp1bi

Description: Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020)

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

Step	Hyp	Ref	Expression
1		dfbi2	$⊢ (if- (φ, χ, θ) \leftrightarrow if- (ψ, χ, θ)) \leftrightarrow ((if- (φ, χ, θ) \to if- (ψ, χ, θ)) \land (if- (ψ, χ, θ) \to if- (φ, χ, θ)))$
2		ifpim1g	$⊢ (if- (φ, χ, θ) \to if- (ψ, χ, θ)) \leftrightarrow (((ψ \to φ) \lor (θ \to χ)) \land ((φ \to ψ) \lor (χ \to θ)))$
3	2	biancomi	$⊢ (if- (φ, χ, θ) \to if- (ψ, χ, θ)) \leftrightarrow (((φ \to ψ) \lor (χ \to θ)) \land ((ψ \to φ) \lor (θ \to χ)))$
4		ifpim1g	$⊢ (if- (ψ, χ, θ) \to if- (φ, χ, θ)) \leftrightarrow (((φ \to ψ) \lor (θ \to χ)) \land ((ψ \to φ) \lor (χ \to θ)))$
5	3 4	anbi12i	$⊢ ((if- (φ, χ, θ) \to if- (ψ, χ, θ)) \land (if- (ψ, χ, θ) \to if- (φ, χ, θ))) \leftrightarrow ((((φ \to ψ) \lor (χ \to θ)) \land ((ψ \to φ) \lor (θ \to χ))) \land (((φ \to ψ) \lor (θ \to χ)) \land ((ψ \to φ) \lor (χ \to θ))))$
6		an42	$⊢ ((((φ \to ψ) \lor (χ \to θ)) \land ((ψ \to φ) \lor (θ \to χ))) \land (((φ \to ψ) \lor (θ \to χ)) \land ((ψ \to φ) \lor (χ \to θ)))) \leftrightarrow ((((φ \to ψ) \lor (χ \to θ)) \land ((φ \to ψ) \lor (θ \to χ))) \land (((ψ \to φ) \lor (χ \to θ)) \land ((ψ \to φ) \lor (θ \to χ))))$
7	1 5 6	3bitri	$⊢ (if- (φ, χ, θ) \leftrightarrow if- (ψ, χ, θ)) \leftrightarrow ((((φ \to ψ) \lor (χ \to θ)) \land ((φ \to ψ) \lor (θ \to χ))) \land (((ψ \to φ) \lor (χ \to θ)) \land ((ψ \to φ) \lor (θ \to χ))))$

Metamath Proof Explorer