MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21nii Structured version   Unicode version

Theorem pm5.21nii 343
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)
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.21nii.3 . 2  |-  ( ps 
->  ( ph  <->  ch )
)
2 pm5.21ni.1 . . 3  |-  ( ph  ->  ps )
3 pm5.21ni.2 . . 3  |-  ( ch 
->  ps )
42, 3pm5.21ni 342 . 2  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
51, 4pm2.61i 158 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  elrabf  3083  sbcco  3175  sbc5  3177  sbcan  3195  sbcor  3197  sbcal  3200  sbcex2  3202  eldif  3322  elun  3480  elin  3522  eluni  4010  eliun  4089  elopab  4454  opelopabsb  4457  elpwun  4748  opeliunxp2  5005  elxp5  5350  tpostpos  6491  ecdmn0  6939  brecop2  6990  elixpsn  7093  bren  7109  elharval  7523  sdom2en01  8174  isfin1-2  8257  wdomac  8397  elwina  8553  elina  8554  lterpq  8839  ltrnq  8848  elnp  8856  elnpi  8857  ltresr  9007  eluz2  10486  dfle2  10732  dflt2  10733  rexanuz2  12145  isstruct2  13470  xpsfrnel2  13782  ismre  13807  isacs  13868  brssc  14006  isfunc  14053  oduclatb  14563  isipodrs  14579  issubg  14936  isnsg  14961  oppgsubm  15150  oppgsubg  15151  isslw  15234  efgrelexlema  15373  dvdsr  15743  isunit  15754  isirred  15796  issubrg  15860  opprsubrg  15881  islss  16003  eltopspOLD  16975  istpsOLD  16977  istopon  16982  basdif0  17010  dis2ndc  17515  elmptrab  17851  isusp  18283  ismet2  18355  isphtpc  19011  elpi1  19062  iscmet  19229  bcthlem1  19269  isvc  22052  isnv  22083  hlimi  22682  h1de2ci  23050  elunop  23367  eldm3  25377  opelco3  25395  elima4  25396  elno  25593  brsset  25726  brbigcup  25735  elfix2  25741  elsingles  25755  imageval  25767  funpartlem  25779  elaltxp  25812  ellines  26078  isfne4  26340  istotbnd  26469  isbnd  26480  isdrngo1  26563  isnacs  26749  sbccomieg  26840  inisegn0  27109  islbs4  27270  elmnc  27309  2reu4  27935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator