Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical conjunction
anbi12i
Next ⟩
anbi12ci
Metamath Proof Explorer
Ascii
Unicode
Theorem
anbi12i
Description:
Conjoin both sides of two equivalences.
(Contributed by
NM
, 12-Mar-1993)
Ref
Expression
Hypotheses
anbi12.1
⊢
φ
↔
ψ
anbi12.2
⊢
χ
↔
θ
Assertion
anbi12i
⊢
φ
∧
χ
↔
ψ
∧
θ
Proof
Step
Hyp
Ref
Expression
1
anbi12.1
⊢
φ
↔
ψ
2
anbi12.2
⊢
χ
↔
θ
3
2
anbi2i
⊢
φ
∧
χ
↔
φ
∧
θ
4
3
1
bianbi
⊢
φ
∧
χ
↔
ψ
∧
θ