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  2909  elrabf  3649  elrab  3652  elrab2w  3657  sbccow  3769  sbcco  3772  sbc5ALT  3775  sbcan  3795  sbcor  3796  sbcal  3805  sbcex2  3806  sbcel1v  3811  sbcreu  3830  eldif  3916  elin  3922  elun  4107  sbccsb2  4402  2reu4  4487  eluni  4877  eliun  4962  sbcbr123  5167  elopab  5513  opelopabsb  5516  opeliunxp2  5826  inisegn0  6102  brfvopabrbr  6990  elpwun  7770  elxp5  7922  opeliunxp2f  8208  tpostpos  8244  ecdmn0  8749  brecop2  8811  elixpsn  8937  bren  8955  0sdom1dom  9209  elharval  9526  brttrcl  9685  sdom2en01  10297  isfin1-2  10380  wdomac  10522  elwina  10682  elina  10683  lterpq  10966  ltrnq  10975  elnp  10983  elnpi  10984  ltresr  11136  eluz2  12879  dfle2  13183  dflt2  13184  rexanuz2  15420  even2n  16417  isstruct2  17226  xpsfrnel2  17635  ismre  17659  isacs  17724  brssc  17888  isfunc  17938  oduclatb  18580  isipodrs  18610  issubg  19215  isnsg  19244  oppgsubm  19455  oppgsubg  19456  isslw  19701  efgrelexlema  19842  dvdsr  20469  isunit  20480  isirred  20526  isrim0  20590  issubrng  20675  opprsubrng  20687  issubrg  20699  opprsubrg  20721  islss  21084  islbs4  22011  istopon  23098  basdif0  23139  dis2ndc  23646  elmptrab  24013  isusp  24447  ismet2  24519  isphtpc  25182  elpi1  25233  iscmet  25472  bcthlem1  25512  elno  27839  elz12s  28694  dfz12s2  28710  wlkcpr  30007  isvcOLD  30960  isnv  30993  hlimi  31569  h1de2ci  31937  elunop  32253  ispcmp  34270  elmpps  36078  eldm3  36266  opelco3  36280  elima4  36281  brsset  36392  brbigcup  36401  elfix2  36407  elsingles  36421  imageval  36433  funpartlem  36447  elaltxp  36480  ellines  36657  isfne4  36884  bj-ismoore  37780  bj-idreseqb  37840  istotbnd  38453  isbnd  38464  isdrngo1  38640  isnacs  43468  sbccomieg  43553  elmnc  43896  ismea  47198  isinv2  49837  oppcinito  50046  oppctermo  50047  oppczeroo  50048  catcsect  50209  lmdfval2  50466  cmdfval2  50467  initocmd  50480  termolmd  50481