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