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  3631  elrab  3634  elrab2w  3638  sbccow  3751  sbcco  3754  sbc5ALT  3757  sbcan  3778  sbcor  3779  sbcal  3788  sbcex2  3789  sbcel1v  3794  sbcreu  3814  eldif  3899  elin  3905  elun  4093  sbccsb2  4377  2reu4  4464  eluni  4853  eliun  4937  sbcbr123  5139  elopab  5482  opelopabsb  5485  opeliunxp2  5793  inisegn0  6063  brfvopabrbr  6944  elpwun  7723  elxp5  7874  opeliunxp2f  8160  tpostpos  8196  ecdmn0  8696  brecop2  8758  elixpsn  8885  bren  8903  0sdom1dom  9156  elharval  9476  brttrcl  9634  sdom2en01  10224  isfin1-2  10307  wdomac  10449  elwina  10609  elina  10610  lterpq  10893  ltrnq  10902  elnp  10910  elnpi  10911  ltresr  11063  eluz2  12794  dfle2  13098  dflt2  13099  rexanuz2  15312  even2n  16311  isstruct2  17119  xpsfrnel2  17528  ismre  17552  isacs  17617  brssc  17781  isfunc  17831  oduclatb  18473  isipodrs  18503  issubg  19102  isnsg  19130  oppgsubm  19337  oppgsubg  19338  isslw  19583  efgrelexlema  19724  dvdsr  20342  isunit  20353  isirred  20399  isrim0  20462  issubrng  20524  opprsubrng  20536  issubrg  20548  opprsubrg  20570  islss  20929  islbs4  21812  istopon  22877  basdif0  22918  dis2ndc  23425  elmptrab  23792  isusp  24226  ismet2  24298  isphtpc  24961  elpi1  25012  iscmet  25251  bcthlem1  25291  elno  27609  elnoOLD  27610  elz12s  28464  dfz12s2  28480  wlkcpr  29697  isvcOLD  30650  isnv  30683  hlimi  31259  h1de2ci  31627  elunop  31943  ispcmp  34001  elmpps  35755  eldm3  35943  opelco3  35957  elima4  35958  brsset  36069  brbigcup  36078  elfix2  36084  elsingles  36098  imageval  36110  funpartlem  36124  elaltxp  36157  ellines  36334  isfne4  36522  bj-ismoore  37417  bj-idreseqb  37477  istotbnd  38090  isbnd  38101  isdrngo1  38277  isnacs  43136  sbccomieg  43221  elmnc  43564  ismea  46879  isinv2  49501  oppcinito  49710  oppctermo  49711  oppczeroo  49712  catcsect  49873  lmdfval2  50130  cmdfval2  50131  initocmd  50144  termolmd  50145