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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  clelab  2904  elrabf  3641  elrab  3644  elrab2w  3649  sbccow  3761  sbcco  3764  sbc5ALT  3767  sbcan  3787  sbcor  3788  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbcreu  3822  eldif  4049  elin  4093  elun  4152  sbccsb2  4394  2reu4  4479  eluni  4869  eliun  4954  sbcbr123  5159  elopab  5500  opelopabsb  5503  opeliunxp2  5814  inisegn0  6095  brfvopabrbr  6991  elpwun  7784  elxp5  7936  opeliunxp2f  8231  tpostpos  8267  ecdmn0  8774  brecop2  8836  elixpsn  8969  bren  8987  0sdom1dom  9241  elharval  9559  brttrcl  9718  sdom2en01  10384  isfin1-2  10467  wdomac  10610  elwina  10775  elina  10776  lterpq  11059  ltrnq  11068  elnp  11076  elnpi  11077  ltresr  11229  eluz2  12975  dfle2  13280  dflt2  13281  rexanuz2  15523  even2n  16518  isstruct2  17333  xpsfrnel2  17742  ismre  17766  isacs  17831  brssc  17995  isfunc  18045  oduclatb  18687  isipodrs  18717  issubg  19342  isnsg  19371  oppgsubm  19582  oppgsubg  19583  isslw  19828  efgrelexlema  19969  dvdsr  20598  isunit  20609  isirred  20655  isrim0  20719  issubrng  20805  opprsubrng  20817  issubrg  20829  opprsubrg  20851  islss  21215  islbs4  22144  istopon  23236  basdif0  23277  dis2ndc  23785  elmptrab  24152  isusp  24586  ismet2  24658  isphtpc  25321  elpi1  25372  iscmet  25611  bcthlem1  25651  elno  28009  elz12s  28864  dfz12s2  28880  wlkcpr  30215  isvcOLD  31187  isnv  31220  hlimi  31796  h1de2ci  32164  elunop  32480  ispcmp  34536  elmpps  36425  eldm3  36619  opelco3  36632  elima4  36633  brsset  36744  brbigcup  36753  elfix2  36759  elsingles  36773  imageval  36785  funpartlem  36799  elaltxp  36833  ellines  37010  isfne4  37221  bj-ismoore  38119  bj-idreseqb  38178  istotbnd  38797  isbnd  38808  isdrngo1  38984  isnacs  43809  sbccomieg  43894  elmnc  44232  ismea  47555  isinv2  50234  oppcinito  50451  oppctermo  50452  oppczeroo  50453  catcsect  50627  lmdfval2  50932  cmdfval2  50933  initocmd  50946  termolmd  50947