Metamath Proof Explorer

Theorem bi123impib

Description: 3impib with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017)

Ref Expression
Hypothesis bi123impib.1 ⊢ φ ↔ ψ ∧ χ ↔ θ
Assertion bi123impib ⊢ φ ∧ ψ ∧ χ → θ

Proof

Step Hyp Ref Expression
1 bi123impib.1 ⊢ φ ↔ ψ ∧ χ ↔ θ
2 1 biimpi ⊢ φ → ψ ∧ χ ↔ θ
3 2 bi23impib ⊢ φ ∧ ψ ∧ χ → θ