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

Theorem pm5.21nii 342
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 341 . 2  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
51, 4pm2.61i 156 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  elrabf  2935  sbcco  3026  sbc5  3028  sbcan  3046  sbcor  3048  sbcal  3051  sbcex2  3053  eldif  3175  elun  3329  elin  3371  eluni  3846  eliun  3925  elopab  4288  opelopabsb  4291  elpwun  4583  opeliunxp2  4840  elxp5  5177  tpostpos  6270  ecdmn0  6718  brecop2  6768  elixpsn  6871  bren  6887  elharval  7293  sdom2en01  7944  isfin1-2  8027  wdomac  8168  elwina  8324  elina  8325  lterpq  8610  ltrnq  8619  elnp  8627  elnpi  8628  ltresr  8778  eluz2  10252  dfle2  10497  dflt2  10498  rexanuz2  11849  isstruct2  13173  xpsfrnel2  13483  ismre  13508  isacs  13569  brssc  13707  isfunc  13754  oduclatb  14264  isipodrs  14280  issubg  14637  isnsg  14662  oppgsubm  14851  oppgsubg  14852  isslw  14935  efgrelexlema  15074  dvdsr  15444  isunit  15455  isirred  15497  issubrg  15561  opprsubrg  15582  islss  15708  eltopspOLD  16672  istpsOLD  16674  istopon  16679  basdif0  16707  dis2ndc  17202  elmptrab  17538  ismet2  17914  isphtpc  18508  elpi1  18559  iscmet  18726  bcthlem1  18762  isvc  21153  isnv  21184  hlimi  21783  h1de2ci  22151  elunop  22468  ballotlemelo  23062  eldm3  24190  elno  24371  brsset  24500  brbigcup  24509  elfix2  24515  dffun10  24524  elsingles  24528  imageval  24540  funpartlem  24552  elaltxp  24581  ellines  24847  isfne4  26372  istotbnd  26596  isbnd  26607  isdrngo1  26690  isnacs  26882  sbccomieg  26973  inisegn0  27243  islbs4  27405  elmnc  27444  2reu4  28071
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 177
  Copyright terms: Public domain W3C validator