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

Theorem pm5.21nii 360
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 359 . 2  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
51, 4pm2.61i 169 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  elrabf  3182  sbcco  3278  sbc5  3280  sbcan  3298  sbcor  3299  sbcal  3305  sbcex2  3306  sbcel1v  3314  sbcreu  3332  eldif  3400  elun  3565  elin  3608  sbccsb2  3798  eluni  4193  eliun  4274  elopab  4709  opelopabsb  4711  opeliunxp2  4978  inisegn0  5206  elpwun  6623  elxp5  6757  opeliunxp2f  6975  tpostpos  7011  ecdmn0  7424  brecop2  7475  elixpsn  7579  bren  7596  elharval  8096  sdom2en01  8750  isfin1-2  8833  wdomac  8973  elwina  9129  elina  9130  lterpq  9413  ltrnq  9422  elnp  9430  elnpi  9431  ltresr  9582  eluz2  11188  dfle2  11469  dflt2  11470  rexanuz2  13489  isstruct2  15208  xpsfrnel2  15549  ismre  15574  isacs  15635  brssc  15797  isfunc  15847  oduclatb  16468  isipodrs  16485  issubg  16895  isnsg  16924  oppgsubm  17091  oppgsubg  17092  isslw  17338  efgrelexlema  17477  dvdsr  17952  isunit  17963  isirred  18005  issubrg  18086  opprsubrg  18107  islss  18236  islbs4  19467  istopon  20017  basdif0  20045  dis2ndc  20552  elmptrab  20919  isusp  21354  ismet2  21426  isphtpc  22103  elpi1  22154  iscmet  22332  bcthlem1  22370  isvc  26281  isnv  26312  hlimi  26922  h1de2ci  27290  elunop  27606  ispcmp  28758  elmpps  30283  eldm3  30473  opelco3  30491  elima4  30492  elno  30604  brsset  30727  brbigcup  30736  elfix2  30742  elsingles  30756  imageval  30768  funpartlem  30780  elaltxp  30813  ellines  30990  isfne4  31067  istotbnd  32165  isbnd  32176  isdrngo1  32259  isnacs  35617  sbccomieg  35707  elmnc  36066  2reu4  38756  1wlkcpr  39831
  Copyright terms: Public domain W3C validator