Theorem pm5.21nii 382

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  elrabf  3675  elrab  3679  sbccow  3794  sbcco  3797  sbc5  3799  sbcan  3820  sbcor  3821  sbcal  3832  sbcex2  3833  sbcel1v  3838  sbcel1vOLD  3839  sbcreu  3858  eldif  3945  elun  4124  elin  4168  sbccsb2  4385  2reu4  4465  elpr2  4584  eluni  4834  eliun  4915  sbcbr123  5112  elopab  5406  opelopabsb  5409  opeliunxp2  5703  inisegn0  5955  brfvopabrbr  6759  elpwun  7485  elxp5  7622  opeliunxp2f  7870  tpostpos  7906  ecdmn0  8330  brecop2  8385  elixpsn  8495  bren  8512  elharval  9021  sdom2en01  9718  isfin1-2  9801  wdomac  9943  elwina  10102  elina  10103  lterpq  10386  ltrnq  10395  elnp  10403  elnpi  10404  ltresr  10556  eluz2  12243  dfle2  12534  dflt2  12535  rexanuz2  14703  even2n  15685  isstruct2  16487  xpsfrnel2  16831  ismre  16855  isacs  16916  brssc  17078  isfunc  17128  oduclatb  17748  isipodrs  17765  issubg  18273  isnsg  18301  oppgsubm  18484  oppgsubg  18485  isslw  18727  efgrelexlema  18869  dvdsr  19390  isunit  19401  isirred  19443  issubrg  19529  opprsubrg  19550  islss  19700  islbs4  20970  istopon  21514  basdif0  21555  dis2ndc  22062  elmptrab  22429  isusp  22864  ismet2  22937  isphtpc  23592  elpi1  23643  iscmet  23881  bcthlem1  23921  wlkcpr  27404  isvcOLD  28350  isnv  28383  hlimi  28959  h1de2ci  29327  elunop  29643  ispcmp  31116  elmpps  32815  eldm3  32992  opelco3  33013  elima4  33014  elno  33148  brsset  33345  brbigcup  33354  elfix2  33360  elsingles  33374  imageval  33386  funpartlem  33398  elaltxp  33431  ellines  33608  isfne4  33683  bj-ismoore  34391  bj-idreseqb  34449  istotbnd  35041  isbnd  35052  isdrngo1  35228  isnacs  39294  sbccomieg  39383  elmnc  39729  ismea  42727