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

Theorem confun5 38402
 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 38382 . . . 4
7 confun5.6 . . . . . 6
8 bicom1 202 . . . . . 6
97, 8ax-mp 5 . . . . 5
109biimpi 197 . . . 4
116, 10ax-mp 5 . . 3
12 confun5.8 . . . 4
13 confun5.5 . . . . . 6
14 bicom1 202 . . . . . 6
1513, 14ax-mp 5 . . . . 5
1615biimpi 197 . . . 4
1712, 16ax-mp 5 . . 3
1811, 172th 242 . 2
19 ax-1 6 . 2
2018, 19ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370 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 188  df-an 372  df-tru 1440  df-fal 1443 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator