Theorem pm5.21nii 381

Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)

Hypotheses

Ref	Expression
pm5.21ni.1	⊢ (𝜑 → 𝜓)
pm5.21ni.2	⊢ (𝜒 → 𝜓)
pm5.21nii.3	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
pm5.21nii	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem pm5.21nii

Step	Hyp	Ref	Expression
1		pm5.21nii.3	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
2		pm5.21ni.1	. . 3 ⊢ (𝜑 → 𝜓)
3		pm5.21ni.2	. . 3 ⊢ (𝜒 → 𝜓)
4	2, 3	pm5.21ni 380	. 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
5	1, 4	pm2.61i 184	1 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  clelab  2905  elrabf  3642  elrab  3645  elrab2w  3650  sbccow  3762  sbcco  3765  sbc5ALT  3768  sbcan  3788  sbcor  3789  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcreu  3823  eldif  3909  elin  3915  elun  4100  sbccsb2  4395  2reu4  4480  eluni  4870  eliun  4955  sbcbr123  5159  elopab  5501  opelopabsb  5504  opeliunxp2  5815  inisegn0  6096  brfvopabrbr  6988  elpwun  7781  elxp5  7933  opeliunxp2f  8220  tpostpos  8256  ecdmn0  8763  brecop2  8825  elixpsn  8958  bren  8976  0sdom1dom  9230  elharval  9548  brttrcl  9707  sdom2en01  10373  isfin1-2  10456  wdomac  10599  elwina  10764  elina  10765  lterpq  11048  ltrnq  11057  elnp  11065  elnpi  11066  ltresr  11218  eluz2  12964  dfle2  13269  dflt2  13270  rexanuz2  15510  even2n  16505  isstruct2  17320  xpsfrnel2  17729  ismre  17753  isacs  17818  brssc  17982  isfunc  18032  oduclatb  18674  isipodrs  18704  issubg  19329  isnsg  19358  oppgsubm  19569  oppgsubg  19570  isslw  19815  efgrelexlema  19956  dvdsr  20585  isunit  20596  isirred  20642  isrim0  20706  issubrng  20792  opprsubrng  20804  issubrg  20816  opprsubrg  20838  islss  21202  islbs4  22131  istopon  23223  basdif0  23264  dis2ndc  23772  elmptrab  24139  isusp  24573  ismet2  24645  isphtpc  25308  elpi1  25359  iscmet  25598  bcthlem1  25638  elno  27996  elz12s  28851  dfz12s2  28867  wlkcpr  30202  isvcOLD  31174  isnv  31207  hlimi  31783  h1de2ci  32151  elunop  32467  ispcmp  34482  elmpps  36317  eldm3  36505  opelco3  36519  elima4  36520  brsset  36631  brbigcup  36640  elfix2  36646  elsingles  36660  imageval  36672  funpartlem  36686  elaltxp  36720  ellines  36897  isfne4  37108  bj-ismoore  38006  bj-idreseqb  38064  istotbnd  38683  isbnd  38694  isdrngo1  38870  isnacs  43694  sbccomieg  43779  elmnc  44122  ismea  47430  isinv2  50103  oppcinito  50312  oppctermo  50313  oppczeroo  50314  catcsect  50475  lmdfval2  50732  cmdfval2  50733  initocmd  50746  termolmd  50747