Theorem: Smt.Reconstruct.Prop.congrIte (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
⊢ c₁ = c₂ → t₁ = t₂ → e₁ = e₂ → (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
Tactic:
intros h₁ h₂ h₃
State after:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
h₁ : c₁ = c₂
h₂ : t₁ = t₂
h₃ : e₁ = e₂
⊢ (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂

State before:
c₁ c₂ : Prop
α : Sort u_1
inst✝¹ : Decidable c₁
inst✝ : Decidable c₂
t₁ t₂ e₁ e₂ : α
h₁ : c₁ = c₂
h₂ : t₁ = t₂
h₃ : e₁ = e₂
⊢ (if c₁ then t₁ else e₁) = if c₂ then t₂ else e₂
Tactic:
simp only [h₁, h₂, h₃]
State after:
no goals