Theorem pm5.21nii 380

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  clelab  2884  elrabf  3621  elrab  3625  sbccow  3740  sbcco  3743  sbc5ALT  3746  sbcan  3769  sbcor  3770  sbcal  3781  sbcex2  3782  sbcel1v  3788  sbcreu  3810  eldif  3898  elin  3904  elun  4084  sbccsb2  4369  2reu4  4458  elpr2OLD  4588  eluni  4843  eliun  4929  sbcbr123  5129  elopab  5441  opelopabsb  5444  opeliunxp2  5750  inisegn0  6009  brfvopabrbr  6881  elpwun  7628  elxp5  7779  opeliunxp2f  8035  tpostpos  8071  ecdmn0  8554  brecop2  8609  elixpsn  8734  bren  8752  brenOLD  8753  elharval  9329  brttrcl  9480  sdom2en01  10067  isfin1-2  10150  wdomac  10292  elwina  10451  elina  10452  lterpq  10735  ltrnq  10744  elnp  10752  elnpi  10753  ltresr  10905  eluz2  12597  dfle2  12890  dflt2  12891  rexanuz2  15070  even2n  16060  isstruct2  16859  xpsfrnel2  17284  ismre  17308  isacs  17369  brssc  17535  isfunc  17588  oduclatb  18234  isipodrs  18264  issubg  18764  isnsg  18792  oppgsubm  18978  oppgsubg  18979  isslw  19222  efgrelexlema  19364  dvdsr  19897  isunit  19908  isirred  19950  issubrg  20033  opprsubrg  20054  islss  20205  islbs4  21048  istopon  22070  basdif0  22112  dis2ndc  22620  elmptrab  22987  isusp  23422  ismet2  23495  isphtpc  24166  elpi1  24217  iscmet  24457  bcthlem1  24497  wlkcpr  28005  isvcOLD  28950  isnv  28983  hlimi  29559  h1de2ci  29927  elunop  30243  ispcmp  31816  elmpps  33544  eldm3  33737  opelco3  33758  elima4  33759  elno  33858  brsset  34200  brbigcup  34209  elfix2  34215  elsingles  34229  imageval  34241  funpartlem  34253  elaltxp  34286  ellines  34463  isfne4  34538  bj-ismoore  35285  bj-idreseqb  35343  istotbnd  35936  isbnd  35947  isdrngo1  36123  elrab2w  40174  isnacs  40533  sbccomieg  40622  elmnc  40968  ismea  43996