Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Anthony Hart
Propositional Calculus
nabi2i
Next ⟩
nabi12i
Metamath Proof Explorer
Ascii
Unicode
Theorem
nabi2i
Description:
Constructor rule for
-/\
.
(Contributed by
Anthony Hart
, 2-Sep-2011)
Ref
Expression
Hypotheses
nabi2i.1
⊢
φ
↔
ψ
nabi2i.2
⊢
χ
⊼
ψ
Assertion
nabi2i
⊢
χ
⊼
φ
Proof
Step
Hyp
Ref
Expression
1
nabi2i.1
⊢
φ
↔
ψ
2
nabi2i.2
⊢
χ
⊼
ψ
3
1
bicomi
⊢
ψ
↔
φ
4
3
nanbi2i
⊢
χ
⊼
ψ
↔
χ
⊼
φ
5
2
4
mpbi
⊢
χ
⊼
φ