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  2873  elrabf  3655  elrab  3659  elrab2w  3663  sbccow  3776  sbcco  3779  sbc5ALT  3782  sbcan  3803  sbcor  3804  sbcal  3813  sbcex2  3814  sbcel1v  3819  sbcreu  3839  eldif  3924  elin  3930  elun  4116  sbccsb2  4400  2reu4  4486  eluni  4874  eliun  4959  sbcbr123  5161  elopab  5487  opelopabsb  5490  opeliunxp2  5802  inisegn0  6069  brfvopabrbr  6965  elpwun  7745  elxp5  7899  opeliunxp2f  8189  tpostpos  8225  ecdmn0  8723  brecop2  8784  elixpsn  8910  bren  8928  0sdom1dom  9185  elharval  9514  brttrcl  9666  sdom2en01  10255  isfin1-2  10338  wdomac  10480  elwina  10639  elina  10640  lterpq  10923  ltrnq  10932  elnp  10940  elnpi  10941  ltresr  11093  eluz2  12799  dfle2  13107  dflt2  13108  rexanuz2  15316  even2n  16312  isstruct2  17119  xpsfrnel2  17527  ismre  17551  isacs  17612  brssc  17776  isfunc  17826  oduclatb  18466  isipodrs  18496  issubg  19058  isnsg  19087  oppgsubm  19294  oppgsubg  19295  isslw  19538  efgrelexlema  19679  dvdsr  20271  isunit  20282  isirred  20328  isrim0  20392  issubrng  20456  opprsubrng  20468  issubrg  20480  opprsubrg  20502  islss  20840  islbs4  21741  istopon  22799  basdif0  22840  dis2ndc  23347  elmptrab  23714  isusp  24149  ismet2  24221  isphtpc  24893  elpi1  24945  iscmet  25184  bcthlem1  25224  elno  27557  elnoOLD  27558  elzs12  28337  wlkcpr  29557  isvcOLD  30508  isnv  30541  hlimi  31117  h1de2ci  31485  elunop  31801  ispcmp  33847  elmpps  35560  eldm3  35748  opelco3  35762  elima4  35763  brsset  35877  brbigcup  35886  elfix2  35892  elsingles  35906  imageval  35918  funpartlem  35930  elaltxp  35963  ellines  36140  isfne4  36328  bj-ismoore  37093  bj-idreseqb  37151  istotbnd  37763  isbnd  37774  isdrngo1  37950  isnacs  42692  sbccomieg  42781  elmnc  43125  ismea  46449  isinv2  49015  oppcinito  49224  oppctermo  49225  oppczeroo  49226  catcsect  49387  lmdfval2  49644  cmdfval2  49645  initocmd  49658  termolmd  49659