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  2880  elrabf  3643  elrab  3646  elrab2w  3650  sbccow  3763  sbcco  3766  sbc5ALT  3769  sbcan  3790  sbcor  3791  sbcal  3800  sbcex2  3801  sbcel1v  3806  sbcreu  3826  eldif  3911  elin  3917  elun  4105  sbccsb2  4389  2reu4  4477  eluni  4866  eliun  4950  sbcbr123  5152  elopab  5475  opelopabsb  5478  opeliunxp2  5787  inisegn0  6057  brfvopabrbr  6938  elpwun  7714  elxp5  7865  opeliunxp2f  8152  tpostpos  8188  ecdmn0  8687  brecop2  8748  elixpsn  8875  bren  8893  0sdom1dom  9146  elharval  9466  brttrcl  9622  sdom2en01  10212  isfin1-2  10295  wdomac  10437  elwina  10597  elina  10598  lterpq  10881  ltrnq  10890  elnp  10898  elnpi  10899  ltresr  11051  eluz2  12757  dfle2  13061  dflt2  13062  rexanuz2  15273  even2n  16269  isstruct2  17076  xpsfrnel2  17485  ismre  17509  isacs  17574  brssc  17738  isfunc  17788  oduclatb  18430  isipodrs  18460  issubg  19056  isnsg  19084  oppgsubm  19291  oppgsubg  19292  isslw  19537  efgrelexlema  19678  dvdsr  20298  isunit  20309  isirred  20355  isrim0  20418  issubrng  20480  opprsubrng  20492  issubrg  20504  opprsubrg  20526  islss  20885  islbs4  21787  istopon  22856  basdif0  22897  dis2ndc  23404  elmptrab  23771  isusp  24205  ismet2  24277  isphtpc  24949  elpi1  25001  iscmet  25240  bcthlem1  25280  elno  27613  elnoOLD  27614  elz12s  28468  dfz12s2  28484  wlkcpr  29702  isvcOLD  30654  isnv  30687  hlimi  31263  h1de2ci  31631  elunop  31947  ispcmp  34014  elmpps  35767  eldm3  35955  opelco3  35969  elima4  35970  brsset  36081  brbigcup  36090  elfix2  36096  elsingles  36110  imageval  36122  funpartlem  36136  elaltxp  36169  ellines  36346  isfne4  36534  bj-ismoore  37310  bj-idreseqb  37368  istotbnd  37970  isbnd  37981  isdrngo1  38157  isnacs  42946  sbccomieg  43035  elmnc  43378  ismea  46695  isinv2  49271  oppcinito  49480  oppctermo  49481  oppczeroo  49482  catcsect  49643  lmdfval2  49900  cmdfval2  49901  initocmd  49914  termolmd  49915