ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.21ndd Unicode version

Theorem pm5.21ndd 656
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypotheses
Ref Expression
pm5.21ndd.1  |-  ( ph  ->  ( ch  ->  ps ) )
pm5.21ndd.2  |-  ( ph  ->  ( th  ->  ps ) )
pm5.21ndd.3  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.21ndd  |-  ( ph  ->  ( ch  <->  th )
)

Proof of Theorem pm5.21ndd
StepHypRef Expression
1 pm5.21ndd.1 . . . 4  |-  ( ph  ->  ( ch  ->  ps ) )
2 pm5.21ndd.3 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
31, 2syld 44 . . 3  |-  ( ph  ->  ( ch  ->  ( ch 
<->  th ) ) )
43ibd 176 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21ndd.2 . . . . 5  |-  ( ph  ->  ( th  ->  ps ) )
65, 2syld 44 . . . 4  |-  ( ph  ->  ( th  ->  ( ch 
<->  th ) ) )
7 bicom1 129 . . . 4  |-  ( ( ch  <->  th )  ->  ( th 
<->  ch ) )
86, 7syl6 33 . . 3  |-  ( ph  ->  ( th  ->  ( th 
<->  ch ) ) )
98ibd 176 . 2  |-  ( ph  ->  ( th  ->  ch ) )
104, 9impbid 127 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.21nd  863  sbcrext  2916  rmob  2931  epelg  4117  eqbrrdva  4606  relbrcnvg  4811  fmptco  5464  ovelrn  5793  brtpos2  6016  elpmg  6421  brdomg  6465  genpelvl  7071  genpelvu  7072  fzoval  9559  clim  10669
  Copyright terms: Public domain W3C validator