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