Theorem mercolem4
Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2.
(Contributed by Anthony Hart, 16-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
Proof
l0
merco2
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l1
merco2
\( \vdash (((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
l2
merco2
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \rightarrow \chi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
mercolem1
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \rightarrow \chi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \theta \rightarrow \chi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
l4
ax-mp l2 _
\( \vdash ((\bot \rightarrow \varphi) \rightarrow \theta \rightarrow \chi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
mercolem1
\( \vdash (((\bot \rightarrow \varphi) \rightarrow \theta \rightarrow \chi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow (\theta \rightarrow \chi) \rightarrow (\bot \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
l6
ax-mp l4 _
\( \vdash (\theta \rightarrow \chi) \rightarrow (\bot \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
merco2
\( \vdash ((\theta \rightarrow \chi) \rightarrow (\bot \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow (((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \)
l8
ax-mp l6 _
\( \vdash (((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \)
mercolem3
\( \vdash ((((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta) \rightarrow (((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow (\bot \rightarrow \varphi) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \)
l10
ax-mp l8 _
\( \vdash (((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow (\bot \rightarrow \varphi) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta \)
merco2
\( \vdash ((((\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow \theta) \rightarrow (\bot \rightarrow \varphi) \rightarrow ((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta) \rightarrow ((((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
ax-mp l10 _
\( \vdash ((((\eta \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \theta) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
ax-mp l1 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
ax-mp l0 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\theta \rightarrow \eta \rightarrow \varphi) \rightarrow ((\theta \rightarrow \chi) \rightarrow \varphi) \rightarrow \tau \rightarrow \eta \rightarrow \varphi \)
ax-mp l0 _