Users' Mathboxes 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 31497
Description: In this proof, the use of the syntactic theorem bj-0 31496 allows to reduce the total length by one (non-essential) step. See also the section comment and the comment of bj-0 31496. Since bj-0 31496 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 31496 as a theorem referencing it). The full proof reads $= wph wps wch bj-0 id $. (while, without using bj-0 31496, 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 1860 or wel 1977). 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 31497 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