Metamath Proof Explorer

Theorem dedlem0a

Description: Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 4-Dec-2012)

Ref Expression
Assertion dedlem0a ⊢ φ → ψ ↔ χ → φ → ψ ∧ φ

Proof

Step Hyp Ref Expression
1 iba ⊢ φ → ψ ↔ ψ ∧ φ
2 biimt ⊢ χ → φ → ψ ∧ φ ↔ χ → φ → ψ ∧ φ
3 2 jarri ⊢ φ → ψ ∧ φ ↔ χ → φ → ψ ∧ φ
4 1 3 bitrd ⊢ φ → ψ ↔ χ → φ → ψ ∧ φ