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

Theorem pm5.21nii 343
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 342 . 2  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
51, 4pm2.61i 158 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  elrabf  3034  sbcco  3126  sbc5  3128  sbcan  3146  sbcor  3148  sbcal  3151  sbcex2  3153  eldif  3273  elun  3431  elin  3473  eluni  3960  eliun  4039  elopab  4403  opelopabsb  4406  elpwun  4696  opeliunxp2  4953  elxp5  5298  tpostpos  6435  ecdmn0  6883  brecop2  6934  elixpsn  7037  bren  7053  elharval  7464  sdom2en01  8115  isfin1-2  8198  wdomac  8338  elwina  8494  elina  8495  lterpq  8780  ltrnq  8789  elnp  8797  elnpi  8798  ltresr  8948  eluz2  10426  dfle2  10672  dflt2  10673  rexanuz2  12080  isstruct2  13405  xpsfrnel2  13717  ismre  13742  isacs  13803  brssc  13941  isfunc  13988  oduclatb  14498  isipodrs  14514  issubg  14871  isnsg  14896  oppgsubm  15085  oppgsubg  15086  isslw  15169  efgrelexlema  15308  dvdsr  15678  isunit  15689  isirred  15731  issubrg  15795  opprsubrg  15816  islss  15938  eltopspOLD  16906  istpsOLD  16908  istopon  16913  basdif0  16941  dis2ndc  17444  elmptrab  17780  isusp  18212  ismet2  18272  isphtpc  18890  elpi1  18941  iscmet  19108  bcthlem1  19146  isvc  21908  isnv  21939  hlimi  22538  h1de2ci  22906  elunop  23223  eldm3  25143  elno  25324  brsset  25453  brbigcup  25462  elfix2  25468  dffun10  25477  elsingles  25481  imageval  25493  funpartlem  25505  elaltxp  25534  ellines  25800  isfne4  26040  istotbnd  26169  isbnd  26180  isdrngo1  26263  isnacs  26449  sbccomieg  26540  inisegn0  26809  islbs4  26971  elmnc  27010  2reu4  27636
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 178
  Copyright terms: Public domain W3C validator