Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-1 Structured version   Visualization version   GIF version

Theorem bj-1 32861
 Description: In this proof, the use of the syntactic theorem bj-0 32860 allows to reduce the total length by one (non-essential) step. See also the section comment and the comment of bj-0 32860. Since bj-0 32860 is used in a non-essential step, this use does not appear on this webpage (but the present theorem appears on the webpage for bj-0 32860 as a theorem referencing it). The full proof reads \$= wph wps wch bj-0 id \$. (while, without using bj-0 32860, it would read \$= wph wps wi wch wi id \$.). Now we explain why syntactic theorems are not useful in set.mm. Suppose that the syntactic theorem thm-0 proves that PHI is a well-formed formula, and that thm-0 is used to shorten the proof of thm-1. Assume that PHI does have proper non-atomic subformulas (which is not the case of the formula proved by weq 2040 or wel 2140). Then, the proof of thm-1 does not construct all the proper non-atomic subformulas of PHI (if it did, then using thm-0 would not shorten it). Therefore, thm-1 is a special instance of a more general theorem with essentially the same proof. In the present case, bj-1 32861 is a special instance of id 22. (Contributed by BJ, 24-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
bj-1 (((𝜑𝜓) → 𝜒) → ((𝜑𝜓) → 𝜒))

Proof of Theorem bj-1
StepHypRef Expression
1 id 22 1 (((𝜑𝜓) → 𝜒) → ((𝜑𝜓) → 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator