Theorem pm5.21nii 381

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  clelab  2909  elrabf  3650  elrab  3653  elrab2w  3658  sbccow  3770  sbcco  3773  sbc5ALT  3776  sbcan  3796  sbcor  3797  sbcal  3806  sbcex2  3807  sbcel1v  3812  sbcreu  3832  eldif  3917  elin  3923  elun  4109  sbccsb2  4394  2reu4  4481  eluni  4870  eliun  4955  sbcbr123  5158  elopab  5501  opelopabsb  5504  opeliunxp2  5814  inisegn0  6090  brfvopabrbr  6976  elpwun  7756  elxp5  7908  opeliunxp2f  8194  tpostpos  8230  ecdmn0  8735  brecop2  8797  elixpsn  8923  bren  8941  0sdom1dom  9194  elharval  9511  brttrcl  9670  sdom2en01  10274  isfin1-2  10357  wdomac  10499  elwina  10659  elina  10660  lterpq  10943  ltrnq  10952  elnp  10960  elnpi  10961  ltresr  11113  eluz2  12856  dfle2  13160  dflt2  13161  rexanuz2  15389  even2n  16388  isstruct2  17197  xpsfrnel2  17606  ismre  17630  isacs  17695  brssc  17859  isfunc  17909  oduclatb  18551  isipodrs  18581  issubg  19180  isnsg  19209  oppgsubm  19420  oppgsubg  19421  isslw  19666  efgrelexlema  19807  dvdsr  20432  isunit  20443  isirred  20489  isrim0  20552  issubrng  20620  opprsubrng  20632  issubrg  20644  opprsubrg  20666  islss  21021  islbs4  21939  istopon  23026  basdif0  23067  dis2ndc  23574  elmptrab  23941  isusp  24375  ismet2  24447  isphtpc  25110  elpi1  25161  iscmet  25400  bcthlem1  25440  elno  27764  elz12s  28619  dfz12s2  28635  wlkcpr  29883  isvcOLD  30836  isnv  30869  hlimi  31445  h1de2ci  31813  elunop  32129  ispcmp  34159  elmpps  35931  eldm3  36119  opelco3  36133  elima4  36134  brsset  36245  brbigcup  36254  elfix2  36260  elsingles  36274  imageval  36286  funpartlem  36300  elaltxp  36333  ellines  36510  isfne4  36708  bj-ismoore  37602  bj-idreseqb  37662  istotbnd  38275  isbnd  38286  isdrngo1  38462  isnacs  43292  sbccomieg  43377  elmnc  43720  ismea  47024  isinv2  49656  oppcinito  49865  oppctermo  49866  oppczeroo  49867  catcsect  50028  lmdfval2  50285  cmdfval2  50286  initocmd  50299  termolmd  50300