This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ififcom

Description: Commute two nested conditionals. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Assertion ififcom ⊢ if φ if ψ A B B = if ψ if φ A B B

Proof

Step Hyp Ref Expression
1 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
2 ifbi ⊢ φ ∧ ψ ↔ ψ ∧ φ → if φ ∧ ψ A B = if ψ ∧ φ A B
3 1 2 ax-mp ⊢ if φ ∧ ψ A B = if ψ ∧ φ A B
4 ifan ⊢ if φ ∧ ψ A B = if φ if ψ A B B
5 ifan ⊢ if ψ ∧ φ A B = if ψ if φ A B B
6 3 4 5 3eqtr3i ⊢ if φ if ψ A B B = if ψ if φ A B B