Theorem pm5.21nii 369

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  elrabf  3554  sbcco  3653  sbc5  3655  sbcan  3673  sbcor  3674  sbcal  3680  sbcex2  3681  sbcel1v  3689  sbcreu  3707  eldif  3776  elun  3949  elin  3992  sbccsb2  4200  elpr2  4391  eluni  4629  eliun  4712  sbcbr123  4894  elopab  5175  opelopabsb  5177  opeliunxp2  5459  inisegn0  5704  brfvopabrbr  6497  elpwun  7204  elxp5  7338  opeliunxp2f  7568  tpostpos  7604  ecdmn0  8021  brecop2  8073  brecop2OLD  8074  elixpsn  8181  bren  8198  elharval  8704  sdom2en01  9406  isfin1-2  9489  wdomac  9631  elwina  9790  elina  9791  lterpq  10074  ltrnq  10083  elnp  10091  elnpi  10092  ltresr  10243  eluz2  11906  dfle2  12192  dflt2  12193  rexanuz2  14308  even2n  15282  isstruct2  16074  xpsfrnel2  16426  ismre  16451  isacs  16512  brssc  16674  isfunc  16724  oduclatb  17345  isipodrs  17362  issubg  17792  isnsg  17821  oppgsubm  17989  oppgsubg  17990  isslw  18220  efgrelexlema  18359  dvdsr  18844  isunit  18855  isirred  18897  issubrg  18980  opprsubrg  19001  islss  19135  islbs4  20377  istopon  20926  basdif0  20967  dis2ndc  21473  elmptrab  21840  isusp  22274  ismet2  22347  isphtpc  23002  elpi1  23053  iscmet  23290  bcthlem1  23329  wlkcpr  26748  frgrusgrfrcond  27430  isvcOLD  27759  isnv  27792  hlimi  28370  h1de2ci  28740  elunop  29056  ispcmp  30246  elmpps  31790  eldm3  31970  opelco3  31995  elima4  31996  elno  32117  brsset  32314  brbigcup  32323  elfix2  32329  elsingles  32343  imageval  32355  funpartlem  32367  elaltxp  32400  ellines  32577  isfne4  32653  istotbnd  33876  isbnd  33887  isdrngo1  34063  isnacs  37766  sbccomieg  37856  elmnc  38204  2reu4  41699