Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bisimpd Unicode version

Theorem bisimpd 23136
Description: Removing of a condition for a biconditionnal connective. (Contributed by Thierry Arnoux, 23-Oct-2016.)
Hypotheses
Ref Expression
bisimpd.1  |-  ( ph  ->  ( ps  ->  th )
)
bisimpd.2  |-  ( ph  ->  ( ch  ->  th )
)
bisimpd.3  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
Assertion
Ref Expression
bisimpd  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem bisimpd
StepHypRef Expression
1 bisimpd.1 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
2 bisimpd.3 . . . 4  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
31, 2syld 40 . . 3  |-  ( ph  ->  ( ps  ->  ( ps 
<->  ch ) ) )
43ibd 234 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
5 bisimpd.2 . . . . 5  |-  ( ph  ->  ( ch  ->  th )
)
65, 2syld 40 . . . 4  |-  ( ph  ->  ( ch  ->  ( ps 
<->  ch ) ) )
7 bicom 191 . . . . 5  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
87imbi2i 303 . . . 4  |-  ( ( ch  ->  ( ps  <->  ch ) )  <->  ( ch  ->  ( ch  <->  ps )
) )
96, 8sylib 188 . . 3  |-  ( ph  ->  ( ch  ->  ( ch 
<->  ps ) ) )
109ibd 234 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
114, 10impbid 183 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  issiga  23487  ismeas  23545  isibfm  23608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator