Step
*
of Lemma
not-not-A-B-example
∀[A,B,F:ℙ].  ((((A ∧ B) ∨ (A 
⇒ F) ∨ (B 
⇒ F)) 
⇒ F) 
⇒ F)
BY
{ (Auto THEN BHyp 4 ) }
1
1. [A] : ℙ
2. [B] : ℙ
3. [F] : ℙ
4. ((A ∧ B) ∨ (A 
⇒ F) ∨ (B 
⇒ F)) 
⇒ F@i
⊢ (A ∧ B) ∨ (A 
⇒ F) ∨ (B 
⇒ F)
Latex:
Latex:
\mforall{}[A,B,F:\mBbbP{}].    ((((A  \mwedge{}  B)  \mvee{}  (A  {}\mRightarrow{}  F)  \mvee{}  (B  {}\mRightarrow{}  F))  {}\mRightarrow{}  F)  {}\mRightarrow{}  F)
By
Latex:
(Auto  THEN  BHyp  4  )
Home
Index