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  2881  elrabf  3632  elrab  3635  elrab2w  3639  sbccow  3752  sbcco  3755  sbc5ALT  3758  sbcan  3779  sbcor  3780  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbcreu  3815  eldif  3900  elin  3906  elun  4094  sbccsb2  4378  2reu4  4465  eluni  4854  eliun  4938  sbcbr123  5140  elopab  5475  opelopabsb  5478  opeliunxp2  5787  inisegn0  6057  brfvopabrbr  6938  elpwun  7716  elxp5  7867  opeliunxp2f  8153  tpostpos  8189  ecdmn0  8689  brecop2  8751  elixpsn  8878  bren  8896  0sdom1dom  9149  elharval  9469  brttrcl  9625  sdom2en01  10215  isfin1-2  10298  wdomac  10440  elwina  10600  elina  10601  lterpq  10884  ltrnq  10893  elnp  10901  elnpi  10902  ltresr  11054  eluz2  12785  dfle2  13089  dflt2  13090  rexanuz2  15303  even2n  16302  isstruct2  17110  xpsfrnel2  17519  ismre  17543  isacs  17608  brssc  17772  isfunc  17822  oduclatb  18464  isipodrs  18494  issubg  19093  isnsg  19121  oppgsubm  19328  oppgsubg  19329  isslw  19574  efgrelexlema  19715  dvdsr  20333  isunit  20344  isirred  20390  isrim0  20453  issubrng  20515  opprsubrng  20527  issubrg  20539  opprsubrg  20561  islss  20920  islbs4  21822  istopon  22887  basdif0  22928  dis2ndc  23435  elmptrab  23802  isusp  24236  ismet2  24308  isphtpc  24971  elpi1  25022  iscmet  25261  bcthlem1  25301  elno  27623  elnoOLD  27624  elz12s  28478  dfz12s2  28494  wlkcpr  29712  isvcOLD  30665  isnv  30698  hlimi  31274  h1de2ci  31642  elunop  31958  ispcmp  34017  elmpps  35771  eldm3  35959  opelco3  35973  elima4  35974  brsset  36085  brbigcup  36094  elfix2  36100  elsingles  36114  imageval  36126  funpartlem  36140  elaltxp  36173  ellines  36350  isfne4  36538  bj-ismoore  37433  bj-idreseqb  37493  istotbnd  38104  isbnd  38115  isdrngo1  38291  isnacs  43150  sbccomieg  43239  elmnc  43582  ismea  46897  isinv2  49513  oppcinito  49722  oppctermo  49723  oppczeroo  49724  catcsect  49885  lmdfval2  50142  cmdfval2  50143  initocmd  50156  termolmd  50157