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

Theorem pm5.21ndd 705
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 45 . . 3  |-  ( ph  ->  ( ch  ->  ( ch 
<->  th ) ) )
43ibd 178 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21ndd.2 . . . . 5  |-  ( ph  ->  ( th  ->  ps ) )
65, 2syld 45 . . . 4  |-  ( ph  ->  ( th  ->  ( ch 
<->  th ) ) )
7 bicom1 131 . . . 4  |-  ( ( ch  <->  th )  ->  ( th 
<->  ch ) )
86, 7syl6 33 . . 3  |-  ( ph  ->  ( th  ->  ( th 
<->  ch ) ) )
98ibd 178 . 2  |-  ( ph  ->  ( th  ->  ch ) )
104, 9impbid 129 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.21nd  916  sbcrext  3041  rmob  3056  epelg  4291  eqbrrdva  4798  elrelimasn  4995  relbrcnvg  5008  fmptco  5683  ovelrn  6023  brtpos2  6252  elpmg  6664  brdomg  6748  elfi2  6971  genpelvl  7511  genpelvu  7512  fzoval  10148  clim  11289  dvdsaddre2b  11848  pceu  12295  mndpropd  12841  issubg3  13052  dvdsrd  13263  subrgpropd  13369  lmodprop2d  13438  cnrest2  13739  cnptoprest2  13743  lmss  13749  reopnap  14041  limcdifap  14134
  Copyright terms: Public domain W3C validator