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  2873  elrabf  3646  elrab  3650  elrab2w  3654  sbccow  3767  sbcco  3770  sbc5ALT  3773  sbcan  3794  sbcor  3795  sbcal  3804  sbcex2  3805  sbcel1v  3810  sbcreu  3830  eldif  3915  elin  3921  elun  4106  sbccsb2  4390  2reu4  4476  eluni  4864  eliun  4948  sbcbr123  5149  elopab  5474  opelopabsb  5477  opeliunxp2  5785  inisegn0  6053  brfvopabrbr  6931  elpwun  7709  elxp5  7863  opeliunxp2f  8150  tpostpos  8186  ecdmn0  8684  brecop2  8745  elixpsn  8871  bren  8889  0sdom1dom  9145  elharval  9472  brttrcl  9628  sdom2en01  10215  isfin1-2  10298  wdomac  10440  elwina  10599  elina  10600  lterpq  10883  ltrnq  10892  elnp  10900  elnpi  10901  ltresr  11053  eluz2  12759  dfle2  13067  dflt2  13068  rexanuz2  15275  even2n  16271  isstruct2  17078  xpsfrnel2  17486  ismre  17510  isacs  17575  brssc  17739  isfunc  17789  oduclatb  18431  isipodrs  18461  issubg  19023  isnsg  19052  oppgsubm  19259  oppgsubg  19260  isslw  19505  efgrelexlema  19646  dvdsr  20265  isunit  20276  isirred  20322  isrim0  20386  issubrng  20450  opprsubrng  20462  issubrg  20474  opprsubrg  20496  islss  20855  islbs4  21757  istopon  22815  basdif0  22856  dis2ndc  23363  elmptrab  23730  isusp  24165  ismet2  24237  isphtpc  24909  elpi1  24961  iscmet  25200  bcthlem1  25240  elno  27573  elnoOLD  27574  elzs12  28368  wlkcpr  29592  isvcOLD  30541  isnv  30574  hlimi  31150  h1de2ci  31518  elunop  31834  ispcmp  33826  elmpps  35548  eldm3  35736  opelco3  35750  elima4  35751  brsset  35865  brbigcup  35874  elfix2  35880  elsingles  35894  imageval  35906  funpartlem  35918  elaltxp  35951  ellines  36128  isfne4  36316  bj-ismoore  37081  bj-idreseqb  37139  istotbnd  37751  isbnd  37762  isdrngo1  37938  isnacs  42680  sbccomieg  42769  elmnc  43112  ismea  46436  isinv2  49015  oppcinito  49224  oppctermo  49225  oppczeroo  49226  catcsect  49387  lmdfval2  49644  cmdfval2  49645  initocmd  49658  termolmd  49659