MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lukshefth2 Structured version   Visualization version   GIF version

Theorem lukshefth2 1768
Description: Lemma for renicax 1769. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
lukshefth2 ((𝜏𝜃) ⊼ ((𝜃𝜏) ⊼ (𝜃𝜏)))

Proof of Theorem lukshefth2
StepHypRef Expression
1 lukshef-ax1 1766 . . . 4 ((𝜓 ⊼ (𝜒𝜑)) ⊼ ((𝜃 ⊼ (𝜃𝜃)) ⊼ ((𝜃𝜒) ⊼ ((𝜓𝜃) ⊼ (𝜓𝜃)))))
2 lukshef-ax1 1766 . . . 4 (((𝜓 ⊼ (𝜒𝜑)) ⊼ ((𝜃 ⊼ (𝜃𝜃)) ⊼ ((𝜃𝜒) ⊼ ((𝜓𝜃) ⊼ (𝜓𝜃))))) ⊼ ((𝜃 ⊼ (𝜃𝜃)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃)))))
31, 2nic-mp 1743 . . 3 ((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃)))
4 lukshefth1 1767 . . . 4 ((((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (𝜑 ⊼ (𝜑𝜑)))
5 lukshef-ax1 1766 . . . . 5 (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ ((𝜑 ⊼ (𝜑𝜑)) ⊼ ((𝜑 ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃)) ⊼ (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ 𝜑) ⊼ ((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ 𝜑)))))
6 lukshef-ax1 1766 . . . . 5 ((((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ ((𝜑 ⊼ (𝜑𝜑)) ⊼ ((𝜑 ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃)) ⊼ (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ 𝜑) ⊼ ((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ 𝜑))))) ⊼ (((((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ ((((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))))) ⊼ (((((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (𝜑 ⊼ (𝜑𝜑))) ⊼ ((((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃)))) ⊼ (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))))))))
75, 6nic-mp 1743 . . . 4 (((((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (𝜑 ⊼ (𝜑𝜑))) ⊼ ((((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃)))) ⊼ (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))))))
84, 7nic-mp 1743 . . 3 (((𝜃 ⊼ (𝜃 ⊼ (𝜃𝜃))) ⊼ (((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃) ⊼ ((𝜓 ⊼ (𝜒𝜑)) ⊼ 𝜃))) ⊼ (((𝜏𝜑) ⊼ ((𝜑𝜏) ⊼ (𝜑𝜏))) ⊼ (𝜃 ⊼ (𝜃𝜃))))
93, 8nic-mp 1743 . 2 (𝜃 ⊼ (𝜃𝜃))
10 lukshef-ax1 1766 . 2 ((𝜃 ⊼ (𝜃𝜃)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ ((𝜏𝜃) ⊼ ((𝜃𝜏) ⊼ (𝜃𝜏)))))
119, 10nic-mp 1743 1 ((𝜏𝜃) ⊼ ((𝜃𝜏) ⊼ (𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wnan 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 383  df-nan 1595
This theorem is referenced by:  renicax  1769
  Copyright terms: Public domain W3C validator