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

Theorem pm5.21nii 693
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypotheses
Ref Expression
pm5.21ni.1  |-  ( ph  ->  ps )
pm5.21ni.2  |-  ( ch 
->  ps )
pm5.21nii.3  |-  ( ps 
->  ( ph  <->  ch )
)
Assertion
Ref Expression
pm5.21nii  |-  ( ph  <->  ch )

Proof of Theorem pm5.21nii
StepHypRef Expression
1 pm5.21ni.1 . . . 4  |-  ( ph  ->  ps )
2 pm5.21nii.3 . . . 4  |-  ( ps 
->  ( ph  <->  ch )
)
31, 2syl 14 . . 3  |-  ( ph  ->  ( ph  <->  ch )
)
43ibi 175 . 2  |-  ( ph  ->  ch )
5 pm5.21ni.2 . . . 4  |-  ( ch 
->  ps )
65, 2syl 14 . . 3  |-  ( ch 
->  ( ph  <->  ch )
)
76ibir 176 . 2  |-  ( ch 
->  ph )
84, 7impbii 125 1  |-  ( ph  <->  ch )
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:  anxordi  1378  elrabf  2838  sbcco  2930  sbc5  2932  sbcan  2951  sbcor  2953  sbcal  2960  sbcex2  2962  sbcel1v  2971  eldif  3080  elun  3217  elin  3259  eluni  3739  eliun  3817  elopab  4180  opelopabsb  4182  opeliunxp  4594  opeliunxp2  4679  elxp4  5026  elxp5  5027  fsn2  5594  isocnv2  5713  elxp6  6067  elxp7  6068  opeliunxp2f  6135  brtpos2  6148  tpostpos  6161  ecdmn0m  6471  elixpsn  6629  bren  6641  omniwomnimkv  7039  elinp  7294  recexprlemell  7442  recexprlemelu  7443  gt0srpr  7568  ltresr  7659  eluz2  9344  elfz2  9809  rexanuz2  10775  even2n  11582  infssuzex  11653  istopon  12194  ishmeo  12487  ismet2  12537
  Copyright terms: Public domain W3C validator