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

Theorem confun4 38401
 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 202 . . . . . . . 8
97, 8ax-mp 5 . . . . . . 7
109biimpi 197 . . . . . 6
116, 10ax-mp 5 . . . . 5
122, 11pm3.2i 456 . . . 4
13 pm3.4 563 . . . 4
1412, 13ax-mp 5 . . 3
155, 14pm3.2i 456 . 2
16 pm3.4 563 . 2
1715, 16ax-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 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator