Theorem pm5.21nii 367

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  elrabf  3329  sbcco  3425  sbc5  3427  sbcan  3445  sbcor  3446  sbcal  3452  sbcex2  3453  sbcel1v  3462  sbcreu  3482  eldif  3550  elun  3715  elin  3758  sbccsb2  3957  elpr2  4147  eluni  4375  eliun  4460  sbcbr123  4636  elopab  4908  opelopabsb  4910  opeliunxp2  5182  inisegn0  5416  elpwun  6869  elxp5  7004  opeliunxp2f  7223  tpostpos  7259  ecdmn0  7676  brecop2  7728  elixpsn  7833  bren  7850  elharval  8351  sdom2en01  9007  isfin1-2  9090  wdomac  9230  elwina  9387  elina  9388  lterpq  9671  ltrnq  9680  elnp  9688  elnpi  9689  ltresr  9840  eluz2  11569  dfle2  11856  dflt2  11857  rexanuz2  13937  even2n  14904  isstruct2  15704  xpsfrnel2  16048  ismre  16073  isacs  16135  brssc  16297  isfunc  16347  oduclatb  16967  isipodrs  16984  issubg  17417  isnsg  17446  oppgsubm  17615  oppgsubg  17616  isslw  17846  efgrelexlema  17985  dvdsr  18469  isunit  18480  isirred  18522  issubrg  18603  opprsubrg  18624  islss  18756  islbs4  19990  istopon  20540  basdif0  20568  dis2ndc  21073  elmptrab  21440  isusp  21875  ismet2  21948  isphtpc  22601  elpi1  22653  iscmet  22890  bcthlem1  22929  isvcOLD  26818  isnv  26851  hlimi  27429  h1de2ci  27799  elunop  28115  ispcmp  29252  elmpps  30724  eldm3  30905  opelco3  30923  elima4  30924  elno  31043  brsset  31166  brbigcup  31175  elfix2  31181  elsingles  31195  imageval  31207  funpartlem  31219  elaltxp  31252  ellines  31429  isfne4  31505  istotbnd  32738  isbnd  32749  isdrngo1  32925  isnacs  36285  sbccomieg  36375  elmnc  36725  2reu4  39839  1wlkcpr  40833  isclwwlksng  41196  frgrusgrfrcond  41431