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

Theorem mercolem5 1733
Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1728. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
mercolem5 (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))

Proof of Theorem mercolem5
StepHypRef Expression
1 merco2 1728 . 2 (((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑))))
2 merco2 1728 . . . . 5 (((𝜑𝜑) → ((⊥ → 𝜑) → 𝜃)) → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))
3 mercolem1 1729 . . . . 5 ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜃)) → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))) → (((⊥ → 𝜑) → 𝜃) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))))
42, 3ax-mp 5 . . . 4 (((⊥ → 𝜑) → 𝜃) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))))
5 mercolem2 1730 . . . . 5 (((𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))) → 𝜃) → ((⊥ → 𝜑) → ((⊥ → 𝜑) → 𝜃)))
6 merco2 1728 . . . . 5 ((((𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))) → 𝜃) → ((⊥ → 𝜑) → ((⊥ → 𝜑) → 𝜃))) → ((((⊥ → 𝜑) → 𝜃) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))) → ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))))))
75, 6ax-mp 5 . . . 4 ((((⊥ → 𝜑) → 𝜃) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))) → ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))))))
84, 7ax-mp 5 . . 3 ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))))
91, 8ax-mp 5 . 2 ((((𝜑𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑𝜑) → (𝜑 → (𝜑𝜑)))) → (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑)))))
101, 9ax-mp 5 1 (𝜃 → ((𝜃𝜑) → (𝜏 → (𝜒𝜑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wfal 1540
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 208  df-tru 1531  df-fal 1541
This theorem is referenced by:  mercolem6  1734  mercolem7  1735
  Copyright terms: Public domain W3C validator