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  1334  elrabf  2760  sbcco  2850  sbc5  2852  sbcan  2870  sbcor  2872  sbcal  2879  sbcex2  2881  sbcel1v  2890  eldif  2997  elun  3130  elin  3172  eluni  3641  eliun  3719  elopab  4061  opelopabsb  4063  opeliunxp  4463  opeliunxp2  4546  elxp4  4886  elxp5  4887  fsn2  5436  isocnv2  5554  elxp6  5899  elxp7  5900  brtpos2  5972  tpostpos  5985  ecdmn0m  6288  bren  6418  elinp  6980  recexprlemell  7128  recexprlemelu  7129  gt0srpr  7241  ltresr  7323  eluz2  8960  elfz2  9366  rexanuz2  10323  even2n  10780  infssuzex  10851
  Copyright terms: Public domain W3C validator