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

Theorem pm5.21ndd 706
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  917  sbcrext  3055  rmob  3070  epelg  4308  eqbrrdva  4815  elrelimasn  5012  relbrcnvg  5025  fmptco  5703  ovelrn  6045  brtpos2  6276  elpmg  6690  brdomg  6774  elfi2  7001  genpelvl  7541  genpelvu  7542  fzoval  10178  clim  11321  dvdsaddre2b  11880  pceu  12327  sgrppropd  12876  mndpropd  12901  issubg3  13131  resghm2b  13201  rngpropd  13309  dvdsrd  13444  opprsubrngg  13558  subrngpropd  13563  subrgpropd  13595  lmodprop2d  13664  cnrest2  14193  cnptoprest2  14197  lmss  14203  reopnap  14495  limcdifap  14588
  Copyright terms: Public domain W3C validator