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