Metamath Proof Explorer


Theorem mpbir3and

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014) (Revised by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mpbir3and.1 φ χ
mpbir3and.2 φ θ
mpbir3and.3 φ τ
mpbir3and.4 φ ψ χ θ τ
Assertion mpbir3and φ ψ

Proof

Step Hyp Ref Expression
1 mpbir3and.1 φ χ
2 mpbir3and.2 φ θ
3 mpbir3and.3 φ τ
4 mpbir3and.4 φ ψ χ θ τ
5 1 2 3 3jca φ χ θ τ
6 5 4 mpbird φ ψ