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

Theorem pm5.21ndd 694
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 177 . 2  |-  ( ph  ->  ( ch  ->  th )
)
5 pm5.21ndd.2 . . . . 5  |-  ( ph  ->  ( th  ->  ps ) )
65, 2syld 45 . . . 4  |-  ( ph  ->  ( th  ->  ( ch 
<->  th ) ) )
7 bicom1 130 . . . 4  |-  ( ( ch  <->  th )  ->  ( th 
<->  ch ) )
86, 7syl6 33 . . 3  |-  ( ph  ->  ( th  ->  ( th 
<->  ch ) ) )
98ibd 177 . 2  |-  ( ph  ->  ( th  ->  ch ) )
104, 9impbid 128 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.21nd  901  sbcrext  2986  rmob  3001  epelg  4212  eqbrrdva  4709  relbrcnvg  4918  fmptco  5586  ovelrn  5919  brtpos2  6148  elpmg  6558  brdomg  6642  elfi2  6860  genpelvl  7332  genpelvu  7333  fzoval  9937  clim  11062  cnrest2  12419  cnptoprest2  12423  lmss  12429  reopnap  12721  limcdifap  12814
  Copyright terms: Public domain W3C validator