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  2922  sbcco  3013  sbc5  3015  sbcan  3033  sbcor  3035  sbcal  3038  sbcex2  3040  eldif  3162  elun  3316  elin  3358  eluni  3830  eliun  3909  elopab  4272  opelopabsb  4275  elpwun  4567  opeliunxp2  4824  elxp5  5161  tpostpos  6254  ecdmn0  6702  brecop2  6752  elixpsn  6855  bren  6871  elharval  7277  sdom2en01  7928  isfin1-2  8011  wdomac  8152  elwina  8308  elina  8309  lterpq  8594  ltrnq  8603  elnp  8611  elnpi  8612  ltresr  8762  eluz2  10236  dfle2  10481  dflt2  10482  rexanuz2  11833  isstruct2  13157  xpsfrnel2  13467  ismre  13492  isacs  13553  brssc  13691  isfunc  13738  oduclatb  14248  isipodrs  14264  issubg  14621  isnsg  14646  oppgsubm  14835  oppgsubg  14836  isslw  14919  efgrelexlema  15058  dvdsr  15428  isunit  15439  isirred  15481  issubrg  15545  opprsubrg  15566  islss  15692  eltopspOLD  16656  istpsOLD  16658  istopon  16663  basdif0  16691  dis2ndc  17186  elmptrab  17522  ismet2  17898  isphtpc  18492  elpi1  18543  iscmet  18710  bcthlem1  18746  isvc  21137  isnv  21168  hlimi  21767  h1de2ci  22135  elunop  22452  ballotlemelo  23046  eldm3  24119  elno  24300  brsset  24429  brbigcup  24438  elfix2  24444  dffun10  24453  elsingles  24457  imageval  24469  elaltxp  24509  ellines  24775  isfne4  26269  istotbnd  26493  isbnd  26504  isdrngo1  26587  isnacs  26779  sbccomieg  26870  inisegn0  27140  islbs4  27302  elmnc  27341  2reu4  27968
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