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 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  clelab  2907  elrabf  3648  elrab  3651  elrab2w  3656  sbccow  3768  sbcco  3771  sbc5ALT  3774  sbcan  3794  sbcor  3795  sbcal  3804  sbcex2  3805  sbcel1v  3810  sbcreu  3830  eldif  3916  elin  3922  elun  4108  sbccsb2  4403  2reu4  4486  eluni  4876  eliun  4961  sbcbr123  5166  elopab  5513  opelopabsb  5516  opeliunxp2  5826  inisegn0  6102  brfvopabrbr  6988  elpwun  7769  elxp5  7921  opeliunxp2f  8207  tpostpos  8243  ecdmn0  8748  brecop2  8810  elixpsn  8936  bren  8954  0sdom1dom  9207  elharval  9524  brttrcl  9683  sdom2en01  10287  isfin1-2  10370  wdomac  10512  elwina  10672  elina  10673  lterpq  10956  ltrnq  10965  elnp  10973  elnpi  10974  ltresr  11126  eluz2  12869  dfle2  13173  dflt2  13174  rexanuz2  15403  even2n  16401  isstruct2  17210  xpsfrnel2  17619  ismre  17643  isacs  17708  brssc  17872  isfunc  17922  oduclatb  18564  isipodrs  18594  issubg  19193  isnsg  19222  oppgsubm  19433  oppgsubg  19434  isslw  19679  efgrelexlema  19820  dvdsr  20445  isunit  20456  isirred  20502  isrim0  20565  issubrng  20633  opprsubrng  20645  issubrg  20657  opprsubrg  20679  islss  21036  islbs4  21963  istopon  23050  basdif0  23091  dis2ndc  23598  elmptrab  23965  isusp  24399  ismet2  24471  isphtpc  25134  elpi1  25185  iscmet  25424  bcthlem1  25464  elno  27791  elz12s  28646  dfz12s2  28662  wlkcpr  29959  isvcOLD  30912  isnv  30945  hlimi  31521  h1de2ci  31889  elunop  32205  ispcmp  34228  elmpps  36046  eldm3  36234  opelco3  36248  elima4  36249  brsset  36360  brbigcup  36369  elfix2  36375  elsingles  36389  imageval  36401  funpartlem  36415  elaltxp  36448  ellines  36625  isfne4  36832  bj-ismoore  37728  bj-idreseqb  37788  istotbnd  38401  isbnd  38412  isdrngo1  38588  isnacs  43418  sbccomieg  43503  elmnc  43846  ismea  47148  isinv2  49787  oppcinito  49996  oppctermo  49997  oppczeroo  49998  catcsect  50159  lmdfval2  50416  cmdfval2  50417  initocmd  50430  termolmd  50431