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

Theorem pm5.21nii 353
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 352 . 2  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
51, 4pm2.61i 164 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  elrabf  3212  sbcco  3307  sbc5  3309  sbcan  3327  sbcor  3329  sbcal  3336  sbcex2  3338  sbcel1v  3349  sbcreu  3371  eldif  3436  elun  3595  elin  3637  sbccsb2  3801  eluni  4192  eliun  4273  elopab  4695  opelopabsb  4697  opeliunxp2  5076  elpwun  6489  elxp5  6623  tpostpos  6865  ecdmn0  7243  brecop2  7294  elixpsn  7402  bren  7419  elharval  7879  sdom2en01  8572  isfin1-2  8655  wdomac  8795  elwina  8954  elina  8955  lterpq  9240  ltrnq  9249  elnp  9257  elnpi  9258  ltresr  9408  eluz2  10968  dfle2  11225  dflt2  11226  rexanuz2  12939  isstruct2  14285  xpsfrnel2  14605  ismre  14630  isacs  14691  brssc  14829  isfunc  14876  oduclatb  15416  isipodrs  15433  issubg  15783  isnsg  15812  oppgsubm  15979  oppgsubg  15980  isslw  16211  efgrelexlema  16350  dvdsr  16844  isunit  16855  isirred  16897  issubrg  16971  opprsubrg  16992  islss  17122  islbs4  18370  eltopspOLD  18639  istpsOLD  18641  istopon  18646  basdif0  18674  dis2ndc  19180  elmptrab  19516  isusp  19952  ismet2  20024  isphtpc  20682  elpi1  20733  iscmet  20911  bcthlem1  20951  isvc  24094  isnv  24125  hlimi  24725  h1de2ci  25094  elunop  25411  eldm3  27706  opelco3  27723  elima4  27724  elno  27921  brsset  28054  brbigcup  28063  elfix2  28069  elsingles  28083  imageval  28095  funpartlem  28107  elaltxp  28140  ellines  28317  isfne4  28679  istotbnd  28806  isbnd  28817  isdrngo1  28900  isnacs  29178  sbccomieg  29269  inisegn0  29534  elmnc  29631  2reu4  30152
  Copyright terms: Public domain W3C validator