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

Theorem confun3 38539
Description: Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.)
Hypotheses
Ref Expression
confun3.1  |-  ( ph  <->  ( ch  ->  ps )
)
confun3.2  |-  ( th  <->  -.  ( ch  ->  ( ch  /\  -.  ch )
) )
confun3.3  |-  ( ch 
->  ps )
confun3.4  |-  ( ch 
->  -.  ( ch  ->  ( ch  /\  -.  ch ) ) )
confun3.5  |-  ( ( ch  ->  ps )  ->  ( ( ch  ->  ps )  ->  ps )
)
Assertion
Ref Expression
confun3  |-  ( ch 
->  ( -.  ( ch 
->  ( ch  /\  -.  ch ) )  <->  ( ch  ->  ps ) ) )

Proof of Theorem confun3
StepHypRef Expression
1 confun3.3 . 2  |-  ( ch 
->  ps )
2 confun3.4 . 2  |-  ( ch 
->  -.  ( ch  ->  ( ch  /\  -.  ch ) ) )
3 confun3.5 . 2  |-  ( ( ch  ->  ps )  ->  ( ( ch  ->  ps )  ->  ps )
)
41, 1, 2, 3confun 38537 1  |-  ( ch 
->  ( -.  ( ch 
->  ( ch  /\  -.  ch ) )  <->  ( ch  ->  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371
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 189
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator