Metamath Proof Explorer

Theorem orbi12i

Description: Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypotheses orbi12i.1 φ ψ
orbi12i.2 χ θ
Assertion orbi12i φ χ ψ θ


Step Hyp Ref Expression
1 orbi12i.1 φ ψ
2 orbi12i.2 χ θ
3 2 orbi2i φ χ φ θ
4 1 orbi1i φ θ ψ θ
5 3 4 bitri φ χ ψ θ