Metamath Proof Explorer

Theorem 0funclem

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

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

Proof

Step Hyp Ref Expression
1 0funclem.1 ⊢ φ → ψ ↔ χ ∧ θ ∧ τ
2 0funclem.2 ⊢ χ ↔ η
3 0funclem.3 ⊢ θ ↔ ζ
4 0funclem.4 ⊢ τ
5 df-3an ⊢ χ ∧ θ ∧ τ ↔ χ ∧ θ ∧ τ
6 1 5 bitrdi ⊢ φ → ψ ↔ χ ∧ θ ∧ τ
7 6 rbaibd ⊢ φ ∧ τ → ψ ↔ χ ∧ θ
8 4 7 mpan2 ⊢ φ → ψ ↔ χ ∧ θ
9 2 3 anbi12i ⊢ χ ∧ θ ↔ η ∧ ζ
10 8 9 bitrdi ⊢ φ → ψ ↔ η ∧ ζ