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  3259  sbcco  3354  sbc5  3356  sbcan  3374  sbcor  3376  sbcal  3383  sbcex2  3385  sbcel1v  3396  sbcreu  3418  eldif  3486  elun  3645  elin  3687  sbccsb2  3851  eluni  4248  eliun  4330  elopab  4755  opelopabsb  4757  opeliunxp2  5139  elpwun  6591  elxp5  6726  tpostpos  6972  ecdmn0  7351  brecop2  7402  elixpsn  7505  bren  7522  elharval  7985  sdom2en01  8678  isfin1-2  8761  wdomac  8901  elwina  9060  elina  9061  lterpq  9344  ltrnq  9353  elnp  9361  elnpi  9362  ltresr  9513  eluz2  11084  dfle2  11349  dflt2  11350  rexanuz2  13138  isstruct2  14492  xpsfrnel2  14813  ismre  14838  isacs  14899  brssc  15037  isfunc  15084  oduclatb  15624  isipodrs  15641  issubg  15993  isnsg  16022  oppgsubm  16189  oppgsubg  16190  isslw  16421  efgrelexlema  16560  dvdsr  17076  isunit  17087  isirred  17129  issubrg  17209  opprsubrg  17230  islss  17361  islbs4  18631  eltopspOLD  19183  istpsOLD  19185  istopon  19190  basdif0  19218  dis2ndc  19724  elmptrab  20060  isusp  20496  ismet2  20568  isphtpc  21226  elpi1  21277  iscmet  21455  bcthlem1  21495  isvc  25147  isnv  25178  hlimi  25778  h1de2ci  26147  elunop  26464  eldm3  28765  opelco3  28782  elima4  28783  elno  28980  brsset  29113  brbigcup  29122  elfix2  29128  elsingles  29142  imageval  29154  funpartlem  29166  elaltxp  29199  ellines  29376  isfne4  29739  istotbnd  29866  isbnd  29877  isdrngo1  29960  isnacs  30238  sbccomieg  30328  inisegn0  30593  elmnc  30690  2reu4  31662
  Copyright terms: Public domain W3C validator