Metamath Proof Explorer

Theorem 0funcglem

Description: Lemma for 0funcg . (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses 0funcglem.1 ⊢ φ → ψ ↔ χ ∧ θ ∧ τ
0funcglem.2 ⊢ φ → χ ↔ η
0funcglem.3 ⊢ φ → θ ↔ ζ
0funcglem.4 ⊢ φ → τ
Assertion 0funcglem ⊢ φ → ψ ↔ η ∧ ζ

Proof

Step Hyp Ref Expression
1 0funcglem.1 ⊢ φ → ψ ↔ χ ∧ θ ∧ τ
2 0funcglem.2 ⊢ φ → χ ↔ η
3 0funcglem.3 ⊢ φ → θ ↔ ζ
4 0funcglem.4 ⊢ φ → τ
5 df-3an ⊢ χ ∧ θ ∧ τ ↔ χ ∧ θ ∧ τ
6 1 5 bitrdi ⊢ φ → ψ ↔ χ ∧ θ ∧ τ
7 4 6 mpbiran2d ⊢ φ → ψ ↔ χ ∧ θ
8 2 3 anbi12d ⊢ φ → χ ∧ θ ↔ η ∧ ζ
9 7 8 bitrd ⊢ φ → ψ ↔ η ∧ ζ