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  3051  sbcco  3143  sbc5  3145  sbcan  3163  sbcor  3165  sbcal  3168  sbcex2  3170  eldif  3290  elun  3448  elin  3490  eluni  3978  eliun  4057  elopab  4422  opelopabsb  4425  elpwun  4715  opeliunxp2  4972  elxp5  5317  tpostpos  6458  ecdmn0  6906  brecop2  6957  elixpsn  7060  bren  7076  elharval  7487  sdom2en01  8138  isfin1-2  8221  wdomac  8361  elwina  8517  elina  8518  lterpq  8803  ltrnq  8812  elnp  8820  elnpi  8821  ltresr  8971  eluz2  10450  dfle2  10696  dflt2  10697  rexanuz2  12108  isstruct2  13433  xpsfrnel2  13745  ismre  13770  isacs  13831  brssc  13969  isfunc  14016  oduclatb  14526  isipodrs  14542  issubg  14899  isnsg  14924  oppgsubm  15113  oppgsubg  15114  isslw  15197  efgrelexlema  15336  dvdsr  15706  isunit  15717  isirred  15759  issubrg  15823  opprsubrg  15844  islss  15966  eltopspOLD  16938  istpsOLD  16940  istopon  16945  basdif0  16973  dis2ndc  17476  elmptrab  17812  isusp  18244  ismet2  18316  isphtpc  18972  elpi1  19023  iscmet  19190  bcthlem1  19230  isvc  22013  isnv  22044  hlimi  22643  h1de2ci  23011  elunop  23328  eldm3  25333  elno  25514  brsset  25643  brbigcup  25652  elfix2  25658  dffun10  25667  elsingles  25671  imageval  25683  funpartlem  25695  elaltxp  25724  ellines  25990  isfne4  26239  istotbnd  26368  isbnd  26379  isdrngo1  26462  isnacs  26648  sbccomieg  26739  inisegn0  27008  islbs4  27170  elmnc  27209  2reu4  27835
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