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  3241  sbcco  3336  sbc5  3338  sbcan  3356  sbcor  3358  sbcal  3365  sbcex2  3367  sbcel1v  3378  sbcreu  3400  eldif  3471  elun  3630  elin  3672  sbccsb2  3837  eluni  4237  eliun  4320  elopab  4745  opelopabsb  4747  opeliunxp2  5131  elpwun  6598  elxp5  6730  tpostpos  6977  ecdmn0  7356  brecop2  7407  elixpsn  7510  bren  7527  elharval  7992  sdom2en01  8685  isfin1-2  8768  wdomac  8908  elwina  9067  elina  9068  lterpq  9351  ltrnq  9360  elnp  9368  elnpi  9369  ltresr  9520  eluz2  11098  dfle2  11364  dflt2  11365  rexanuz2  13164  isstruct2  14623  xpsfrnel2  14944  ismre  14969  isacs  15030  brssc  15165  isfunc  15212  oduclatb  15753  isipodrs  15770  issubg  16180  isnsg  16209  oppgsubm  16376  oppgsubg  16377  isslw  16607  efgrelexlema  16746  dvdsr  17274  isunit  17285  isirred  17327  issubrg  17408  opprsubrg  17429  islss  17560  islbs4  18845  eltopspOLD  19397  istpsOLD  19399  istopon  19404  basdif0  19432  dis2ndc  19939  elmptrab  20306  isusp  20742  ismet2  20814  isphtpc  21472  elpi1  21523  iscmet  21701  bcthlem1  21741  isvc  25452  isnv  25483  hlimi  26083  h1de2ci  26452  elunop  26769  ispcmp  27838  elmpps  28911  eldm3  29167  opelco3  29184  elima4  29185  elno  29382  brsset  29515  brbigcup  29524  elfix2  29530  elsingles  29544  imageval  29556  funpartlem  29568  elaltxp  29601  ellines  29778  isfne4  30134  istotbnd  30241  isbnd  30252  isdrngo1  30335  isnacs  30612  sbccomieg  30702  inisegn0  30965  elmnc  31061  2reu4  32149
  Copyright terms: Public domain W3C validator