Theorem pm5.21nii 371

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  elrabf  3586  elrab  3590  sbcco  3699  sbc5  3701  sbcan  3720  sbcor  3721  sbcal  3731  sbcex2  3732  sbcel1v  3737  sbcel1vOLD  3738  sbcreu  3757  eldif  3834  elun  4009  elin  4052  sbccsb2  4265  2reu4  4344  elpr2  4460  eluni  4712  eliun  4793  sbcbr123  4980  elopab  5266  opelopabsb  5268  opeliunxp2  5556  inisegn0  5799  brfvopabrbr  6591  elpwun  7307  elxp5  7442  opeliunxp2f  7678  tpostpos  7714  ecdmn0  8135  brecop2  8190  elixpsn  8297  bren  8314  elharval  8821  sdom2en01  9521  isfin1-2  9604  wdomac  9746  elwina  9905  elina  9906  lterpq  10189  ltrnq  10198  elnp  10206  elnpi  10207  ltresr  10359  eluz2  12063  dfle2  12356  dflt2  12357  rexanuz2  14569  even2n  15550  isstruct2  16348  xpsfrnel2cda  16699  xpsfrnel2  16702  ismre  16732  isacs  16793  brssc  16955  isfunc  17005  oduclatb  17625  isipodrs  17642  issubg  18076  isnsg  18105  oppgsubm  18274  oppgsubg  18275  isslw  18507  efgrelexlema  18648  dvdsr  19132  isunit  19143  isirred  19185  issubrg  19271  opprsubrg  19292  islss  19441  islbs4  20694  istopon  21240  basdif0  21281  dis2ndc  21788  elmptrab  22155  isusp  22589  ismet2  22662  isphtpc  23317  elpi1  23368  iscmet  23606  bcthlem1  23646  wlkcpr  27129  frgrusgrfrcond  27809  isvcOLD  28149  isnv  28182  hlimi  28760  h1de2ci  29130  elunop  29446  ispcmp  30798  elmpps  32373  eldm3  32550  opelco3  32571  elima4  32572  elno  32707  brsset  32904  brbigcup  32913  elfix2  32919  elsingles  32933  imageval  32945  funpartlem  32957  elaltxp  32990  ellines  33167  isfne4  33242  istotbnd  34522  isbnd  34533  isdrngo1  34709  isnacs  38730  sbccomieg  38820  elmnc  39166  ismea  42194