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  3679  elrab  3683  sbccow  3798  sbcco  3801  sbc5  3803  sbcan  3824  sbcor  3825  sbcal  3836  sbcex2  3837  sbcel1v  3842  sbcel1vOLD  3843  sbcreu  3862  eldif  3949  elun  4128  elin  4172  sbccsb2  4389  2reu4  4469  elpr2  4594  eluni  4844  eliun  4926  sbcbr123  5123  elopab  5417  opelopabsb  5420  opeliunxp2  5712  inisegn0  5964  brfvopabrbr  6768  elpwun  7494  elxp5  7631  opeliunxp2f  7879  tpostpos  7915  ecdmn0  8339  brecop2  8394  elixpsn  8504  bren  8521  elharval  9030  sdom2en01  9727  isfin1-2  9810  wdomac  9952  elwina  10111  elina  10112  lterpq  10395  ltrnq  10404  elnp  10412  elnpi  10413  ltresr  10565  eluz2  12252  dfle2  12543  dflt2  12544  rexanuz2  14712  even2n  15694  isstruct2  16496  xpsfrnel2  16840  ismre  16864  isacs  16925  brssc  17087  isfunc  17137  oduclatb  17757  isipodrs  17774  issubg  18282  isnsg  18310  oppgsubm  18493  oppgsubg  18494  isslw  18736  efgrelexlema  18878  dvdsr  19399  isunit  19410  isirred  19452  issubrg  19538  opprsubrg  19559  islss  19709  islbs4  20979  istopon  21523  basdif0  21564  dis2ndc  22071  elmptrab  22438  isusp  22873  ismet2  22946  isphtpc  23601  elpi1  23652  iscmet  23890  bcthlem1  23930  wlkcpr  27413  isvcOLD  28359  isnv  28392  hlimi  28968  h1de2ci  29336  elunop  29652  ispcmp  31125  elmpps  32824  eldm3  33001  opelco3  33022  elima4  33023  elno  33157  brsset  33354  brbigcup  33363  elfix2  33369  elsingles  33383  imageval  33395  funpartlem  33407  elaltxp  33440  ellines  33617  isfne4  33692  bj-ismoore  34401  bj-idreseqb  34459  istotbnd  35051  isbnd  35062  isdrngo1  35238  isnacs  39307  sbccomieg  39396  elmnc  39742  ismea  42740