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  3645  elrab  3648  elrab2w  3652  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3792  sbcor  3793  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcreu  3828  eldif  3913  elin  3919  elun  4107  sbccsb2  4391  2reu4  4479  eluni  4868  eliun  4952  sbcbr123  5154  elopab  5483  opelopabsb  5486  opeliunxp2  5795  inisegn0  6065  brfvopabrbr  6946  elpwun  7724  elxp5  7875  opeliunxp2f  8162  tpostpos  8198  ecdmn0  8698  brecop2  8760  elixpsn  8887  bren  8905  0sdom1dom  9158  elharval  9478  brttrcl  9634  sdom2en01  10224  isfin1-2  10307  wdomac  10449  elwina  10609  elina  10610  lterpq  10893  ltrnq  10902  elnp  10910  elnpi  10911  ltresr  11063  eluz2  12769  dfle2  13073  dflt2  13074  rexanuz2  15285  even2n  16281  isstruct2  17088  xpsfrnel2  17497  ismre  17521  isacs  17586  brssc  17750  isfunc  17800  oduclatb  18442  isipodrs  18472  issubg  19068  isnsg  19096  oppgsubm  19303  oppgsubg  19304  isslw  19549  efgrelexlema  19690  dvdsr  20310  isunit  20321  isirred  20367  isrim0  20430  issubrng  20492  opprsubrng  20504  issubrg  20516  opprsubrg  20538  islss  20897  islbs4  21799  istopon  22868  basdif0  22909  dis2ndc  23416  elmptrab  23783  isusp  24217  ismet2  24289  isphtpc  24961  elpi1  25013  iscmet  25252  bcthlem1  25292  elno  27625  elnoOLD  27626  elz12s  28480  dfz12s2  28496  wlkcpr  29714  isvcOLD  30666  isnv  30699  hlimi  31275  h1de2ci  31643  elunop  31959  ispcmp  34034  elmpps  35786  eldm3  35974  opelco3  35988  elima4  35989  brsset  36100  brbigcup  36109  elfix2  36115  elsingles  36129  imageval  36141  funpartlem  36155  elaltxp  36188  ellines  36365  isfne4  36553  bj-ismoore  37355  bj-idreseqb  37415  istotbnd  38017  isbnd  38028  isdrngo1  38204  isnacs  43058  sbccomieg  43147  elmnc  43490  ismea  46806  isinv2  49382  oppcinito  49591  oppctermo  49592  oppczeroo  49593  catcsect  49754  lmdfval2  50011  cmdfval2  50012  initocmd  50025  termolmd  50026