Metamath Proof Explorer


Theorem biadanii

Description: Inference associated with biadani . Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011) (Proof shortened by BJ, 4-Mar-2023)

Ref Expression
Hypotheses biadani.1 φ ψ
biadanii.2 ψ φ χ
Assertion biadanii φ ψ χ

Proof

Step Hyp Ref Expression
1 biadani.1 φ ψ
2 biadanii.2 ψ φ χ
3 1 biadani ψ φ χ φ ψ χ
4 2 3 mpbi φ ψ χ