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

Theorem confun4 39758
 Description: An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.)
Hypotheses
Ref Expression
confun4.1 𝜑
confun4.2 ((𝜑𝜓) → 𝜓)
confun4.3 (𝜓 → (𝜑𝜒))
confun4.4 ((𝜒𝜃) → ((𝜑𝜃) ↔ 𝜓))
confun4.5 (𝜏 ↔ (𝜒𝜃))
confun4.6 (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))
confun4.7 𝜓
confun4.8 (𝜒𝜃)
Assertion
Ref Expression
confun4 (𝜒 → (𝜓𝜏))

Proof of Theorem confun4
StepHypRef Expression
1 confun4.1 . . . 4 𝜑
2 confun4.7 . . . . 5 𝜓
3 confun4.3 . . . . 5 (𝜓 → (𝜑𝜒))
42, 3ax-mp 5 . . . 4 (𝜑𝜒)
51, 4ax-mp 5 . . 3 𝜒
6 confun4.8 . . . . . 6 (𝜒𝜃)
7 confun4.5 . . . . . . . 8 (𝜏 ↔ (𝜒𝜃))
8 bicom1 210 . . . . . . . 8 ((𝜏 ↔ (𝜒𝜃)) → ((𝜒𝜃) ↔ 𝜏))
97, 8ax-mp 5 . . . . . . 7 ((𝜒𝜃) ↔ 𝜏)
109biimpi 205 . . . . . 6 ((𝜒𝜃) → 𝜏)
116, 10ax-mp 5 . . . . 5 𝜏
122, 11pm3.2i 470 . . . 4 (𝜓𝜏)
13 pm3.4 582 . . . 4 ((𝜓𝜏) → (𝜓𝜏))
1412, 13ax-mp 5 . . 3 (𝜓𝜏)
155, 14pm3.2i 470 . 2 (𝜒 ∧ (𝜓𝜏))
16 pm3.4 582 . 2 ((𝜒 ∧ (𝜓𝜏)) → (𝜒 → (𝜓𝜏)))
1715, 16ax-mp 5 1 (𝜒 → (𝜓𝜏))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator