Metamath Proof Explorer


Theorem nic-isw2

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 ( 𝜓 ⊼ ( 𝜑𝜃 ) )