Theorem pm5.21nii 378

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 377	. 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
5	1, 4	pm2.61i 182	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  clelab  2877  elrabf  3640  elrab  3643  elrab2w  3647  sbccow  3760  sbcco  3763  sbc5ALT  3766  sbcan  3787  sbcor  3788  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbcreu  3823  eldif  3908  elin  3914  elun  4102  sbccsb2  4386  2reu4  4474  eluni  4863  eliun  4947  sbcbr123  5149  elopab  5472  opelopabsb  5475  opeliunxp2  5784  inisegn0  6053  brfvopabrbr  6934  elpwun  7710  elxp5  7861  opeliunxp2f  8148  tpostpos  8184  ecdmn0  8682  brecop2  8743  elixpsn  8869  bren  8887  0sdom1dom  9139  elharval  9456  brttrcl  9612  sdom2en01  10202  isfin1-2  10285  wdomac  10427  elwina  10586  elina  10587  lterpq  10870  ltrnq  10879  elnp  10887  elnpi  10888  ltresr  11040  eluz2  12746  dfle2  13050  dflt2  13051  rexanuz2  15261  even2n  16257  isstruct2  17064  xpsfrnel2  17472  ismre  17496  isacs  17561  brssc  17725  isfunc  17775  oduclatb  18417  isipodrs  18447  issubg  19043  isnsg  19071  oppgsubm  19278  oppgsubg  19279  isslw  19524  efgrelexlema  19665  dvdsr  20284  isunit  20295  isirred  20341  isrim0  20404  issubrng  20466  opprsubrng  20478  issubrg  20490  opprsubrg  20512  islss  20871  islbs4  21773  istopon  22830  basdif0  22871  dis2ndc  23378  elmptrab  23745  isusp  24179  ismet2  24251  isphtpc  24923  elpi1  24975  iscmet  25214  bcthlem1  25254  elno  27587  elnoOLD  27588  elzs12  28386  wlkcpr  29611  isvcOLD  30563  isnv  30596  hlimi  31172  h1de2ci  31540  elunop  31856  ispcmp  33893  elmpps  35640  eldm3  35828  opelco3  35842  elima4  35843  brsset  35954  brbigcup  35963  elfix2  35969  elsingles  35983  imageval  35995  funpartlem  36009  elaltxp  36042  ellines  36219  isfne4  36407  bj-ismoore  37172  bj-idreseqb  37230  istotbnd  37832  isbnd  37843  isdrngo1  38019  isnacs  42824  sbccomieg  42913  elmnc  43256  ismea  46576  isinv2  49154  oppcinito  49363  oppctermo  49364  oppczeroo  49365  catcsect  49526  lmdfval2  49783  cmdfval2  49784  initocmd  49797  termolmd  49798