Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Other axiomatizations related to classical propositional calculus
Derive the Lukasiewicz axioms from Nicod's axiom
nic-imp
Metamath Proof Explorer
Description: Inference for nic-mp using nic-ax as major premise. (Contributed by Jeff Hoffman , 17-Nov-2007) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypothesis
nic-imp.1
⊢ ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) )
Assertion
nic-imp
⊢ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) )
Proof
Step
Hyp
Ref
Expression
1
nic-imp.1
⊢ ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) )
2
nic-ax
⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
3
1 2
nic-mp
⊢ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) )