Description: Lemma for nic-id . Inference used by nic-id . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nic-idlem2.1 | ⊢ ( 𝜂 ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ 𝜃 ) ) | |
| Assertion | nic-idlem2 | ⊢ ( ( 𝜃 ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ 𝜂 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nic-idlem2.1 | ⊢ ( 𝜂 ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ 𝜃 ) ) | |
| 2 | nic-ax | ⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜑 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜑 ) ⊼ ( 𝜑 ⊼ 𝜑 ) ) ) ) ) | |
| 3 | 2 | nic-imp | ⊢ ( ( 𝜃 ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ ( ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ 𝜃 ) ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ 𝜃 ) ) ) |
| 4 | 3 | nic-imp | ⊢ ( ( 𝜂 ⊼ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ 𝜃 ) ) ⊼ ( ( ( 𝜃 ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ 𝜂 ) ⊼ ( ( 𝜃 ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ 𝜂 ) ) ) |
| 5 | 1 4 | nic-mp | ⊢ ( ( 𝜃 ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ 𝜂 ) |