Mathbox for Jarvin Udandy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  confun5 Structured version   Visualization version   GIF version

Theorem confun5 43534
 Description: An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.)
Hypotheses
Ref Expression
confun5.1 𝜑
confun5.2 ((𝜑𝜓) → 𝜓)
confun5.3 (𝜓 → (𝜑𝜒))
confun5.4 ((𝜒𝜃) → ((𝜑𝜃) ↔ 𝜓))
confun5.5 (𝜏 ↔ (𝜒𝜃))
confun5.6 (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))
confun5.7 𝜓
confun5.8 (𝜒𝜃)
Assertion
Ref Expression
confun5 (𝜒 → (𝜂𝜏))

Proof of Theorem confun5
StepHypRef Expression
1 confun5.1 . . . . . 6 𝜑
2 confun5.7 . . . . . . 7 𝜓
3 confun5.3 . . . . . . 7 (𝜓 → (𝜑𝜒))
42, 3ax-mp 5 . . . . . 6 (𝜑𝜒)
51, 4ax-mp 5 . . . . 5 𝜒
65atnaiana 43514 . . . 4 ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))
7 confun5.6 . . . . . 6 (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))
8 bicom1 224 . . . . . 6 ((𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒))) → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ 𝜂))
97, 8ax-mp 5 . . . . 5 (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ 𝜂)
109biimpi 219 . . . 4 (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) → 𝜂)
116, 10ax-mp 5 . . 3 𝜂
12 confun5.8 . . . 4 (𝜒𝜃)
13 confun5.5 . . . . . 6 (𝜏 ↔ (𝜒𝜃))
14 bicom1 224 . . . . . 6 ((𝜏 ↔ (𝜒𝜃)) → ((𝜒𝜃) ↔ 𝜏))
1513, 14ax-mp 5 . . . . 5 ((𝜒𝜃) ↔ 𝜏)
1615biimpi 219 . . . 4 ((𝜒𝜃) → 𝜏)
1712, 16ax-mp 5 . . 3 𝜏
1811, 172th 267 . 2 (𝜂𝜏)
19 ax-1 6 . 2 ((𝜂𝜏) → (𝜒 → (𝜂𝜏)))
2018, 19ax-mp 5 1 (𝜒 → (𝜂𝜏))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400  df-tru 1541  df-fal 1551 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator