Users' Mathboxes 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  |-  ph
confun4.2  |-  ( (
ph  ->  ps )  ->  ps )
confun4.3  |-  ( ps 
->  ( ph  ->  ch ) )
confun4.4  |-  ( ( ch  ->  th )  ->  ( ( ph  ->  th )  <->  ps ) )
confun4.5  |-  ( ta  <->  ( ch  ->  th )
)
confun4.6  |-  ( et  <->  -.  ( ch  ->  ( ch  /\  -.  ch )
) )
confun4.7  |-  ps
confun4.8  |-  ( ch 
->  th )
Assertion
Ref Expression
confun4  |-  ( ch 
->  ( ps  ->  ta ) )

Proof of Theorem confun4
StepHypRef Expression
1 confun4.1 . . . 4  |-  ph
2 confun4.7 . . . . 5  |-  ps
3 confun4.3 . . . . 5  |-  ( ps 
->  ( ph  ->  ch ) )
42, 3ax-mp 5 . . . 4  |-  ( ph  ->  ch )
51, 4ax-mp 5 . . 3  |-  ch
6 confun4.8 . . . . . 6  |-  ( ch 
->  th )
7 confun4.5 . . . . . . . 8  |-  ( ta  <->  ( ch  ->  th )
)
8 bicom1 202 . . . . . . . 8  |-  ( ( ta  <->  ( ch  ->  th ) )  ->  (
( ch  ->  th )  <->  ta ) )
97, 8ax-mp 5 . . . . . . 7  |-  ( ( ch  ->  th )  <->  ta )
109biimpi 197 . . . . . 6  |-  ( ( ch  ->  th )  ->  ta )
116, 10ax-mp 5 . . . . 5  |-  ta
122, 11pm3.2i 456 . . . 4  |-  ( ps 
/\  ta )
13 pm3.4 563 . . . 4  |-  ( ( ps  /\  ta )  ->  ( ps  ->  ta ) )
1412, 13ax-mp 5 . . 3  |-  ( ps 
->  ta )
155, 14pm3.2i 456 . 2  |-  ( ch 
/\  ( ps  ->  ta ) )
16 pm3.4 563 . 2  |-  ( ( ch  /\  ( ps 
->  ta ) )  -> 
( ch  ->  ( ps  ->  ta ) ) )
1715, 16ax-mp 5 1  |-  ( ch 
->  ( ps  ->  ta ) )
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