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

Theorem pm5.21nii 653
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 174 . 2  |-  ( ph  ->  ch )
5 pm5.21ni.2 . . . 4  |-  ( ch 
->  ps )
65, 2syl 14 . . 3  |-  ( ch 
->  ( ph  <->  ch )
)
76ibir 175 . 2  |-  ( ch 
->  ph )
84, 7impbii 124 1  |-  ( ph  <->  ch )
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:  anxordi  1332  elrabf  2748  sbcco  2837  sbc5  2839  sbcan  2857  sbcor  2859  sbcal  2866  sbcex2  2868  sbcel1v  2877  eldif  2983  elun  3114  elin  3156  eluni  3612  eliun  3690  elopab  4021  opelopabsb  4023  opeliunxp  4421  opeliunxp2  4504  elxp4  4838  elxp5  4839  fsn2  5369  isocnv2  5483  elxp6  5827  elxp7  5828  brtpos2  5900  tpostpos  5913  ecdmn0m  6214  bren  6294  elinp  6726  recexprlemell  6874  recexprlemelu  6875  gt0srpr  6987  ltresr  7069  eluz2  8706  elfz2  9112  rexanuz2  10015  even2n  10418  infssuzex  10489
  Copyright terms: Public domain W3C validator