Metamath Proof Explorer

Theorem impbid

Description: Deduce an equivalence from two implications. Deduction associated with impbi and impbii . (Contributed by NM, 24-Jan-1993) Revised to prove it from impbid21d . (Revised by Wolf Lammen, 3-Nov-2012)

Ref Expression
Hypotheses impbid.1 φ ψ χ
impbid.2 φ χ ψ
Assertion impbid φ ψ χ


Step Hyp Ref Expression
1 impbid.1 φ ψ χ
2 impbid.2 φ χ ψ
3 1 2 impbid21d φ φ ψ χ
4 3 pm2.43i φ ψ χ