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  3112  sbcco  3206  sbc5  3208  sbcan  3226  sbcor  3228  sbcal  3235  sbcex2  3237  sbcel1v  3248  sbcreu  3270  eldif  3335  elun  3494  elin  3536  sbccsb2  3700  eluni  4091  eliun  4172  elopab  4594  opelopabsb  4597  opeliunxp2  4974  elpwun  6388  elxp5  6522  tpostpos  6764  ecdmn0  7139  brecop2  7190  elixpsn  7298  bren  7315  elharval  7774  sdom2en01  8467  isfin1-2  8550  wdomac  8690  elwina  8849  elina  8850  lterpq  9135  ltrnq  9144  elnp  9152  elnpi  9153  ltresr  9303  eluz2  10863  dfle2  11120  dflt2  11121  rexanuz2  12833  isstruct2  14179  xpsfrnel2  14499  ismre  14524  isacs  14585  brssc  14723  isfunc  14770  oduclatb  15310  isipodrs  15327  issubg  15674  isnsg  15703  oppgsubm  15870  oppgsubg  15871  isslw  16100  efgrelexlema  16239  dvdsr  16728  isunit  16739  isirred  16781  issubrg  16845  opprsubrg  16866  islss  16994  islbs4  18220  eltopspOLD  18482  istpsOLD  18484  istopon  18489  basdif0  18517  dis2ndc  19023  elmptrab  19359  isusp  19795  ismet2  19867  isphtpc  20525  elpi1  20576  iscmet  20754  bcthlem1  20794  isvc  23894  isnv  23925  hlimi  24525  h1de2ci  24894  elunop  25211  eldm3  27501  opelco3  27518  elima4  27519  elno  27716  brsset  27849  brbigcup  27858  elfix2  27864  elsingles  27878  imageval  27890  funpartlem  27902  elaltxp  27935  ellines  28112  isfne4  28466  istotbnd  28593  isbnd  28604  isdrngo1  28687  isnacs  28965  sbccomieg  29056  inisegn0  29321  elmnc  29418  2reu4  29939
  Copyright terms: Public domain W3C validator