Theorem pm5.21nii 378

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  clelab  2876  elrabf  3644  elrab  3647  elrab2w  3651  sbccow  3764  sbcco  3767  sbc5ALT  3770  sbcan  3791  sbcor  3792  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbcreu  3827  eldif  3912  elin  3918  elun  4103  sbccsb2  4387  2reu4  4473  eluni  4862  eliun  4945  sbcbr123  5145  elopab  5467  opelopabsb  5470  opeliunxp2  5778  inisegn0  6047  brfvopabrbr  6926  elpwun  7702  elxp5  7853  opeliunxp2f  8140  tpostpos  8176  ecdmn0  8674  brecop2  8735  elixpsn  8861  bren  8879  0sdom1dom  9130  elharval  9447  brttrcl  9603  sdom2en01  10193  isfin1-2  10276  wdomac  10418  elwina  10577  elina  10578  lterpq  10861  ltrnq  10870  elnp  10878  elnpi  10879  ltresr  11031  eluz2  12738  dfle2  13046  dflt2  13047  rexanuz2  15257  even2n  16253  isstruct2  17060  xpsfrnel2  17468  ismre  17492  isacs  17557  brssc  17721  isfunc  17771  oduclatb  18413  isipodrs  18443  issubg  19039  isnsg  19068  oppgsubm  19275  oppgsubg  19276  isslw  19521  efgrelexlema  19662  dvdsr  20281  isunit  20292  isirred  20338  isrim0  20401  issubrng  20463  opprsubrng  20475  issubrg  20487  opprsubrg  20509  islss  20868  islbs4  21770  istopon  22828  basdif0  22869  dis2ndc  23376  elmptrab  23743  isusp  24177  ismet2  24249  isphtpc  24921  elpi1  24973  iscmet  25212  bcthlem1  25252  elno  27585  elnoOLD  27586  elzs12  28384  wlkcpr  29608  isvcOLD  30557  isnv  30590  hlimi  31166  h1de2ci  31534  elunop  31850  ispcmp  33868  elmpps  35615  eldm3  35803  opelco3  35817  elima4  35818  brsset  35929  brbigcup  35938  elfix2  35944  elsingles  35958  imageval  35970  funpartlem  35982  elaltxp  36015  ellines  36192  isfne4  36380  bj-ismoore  37145  bj-idreseqb  37203  istotbnd  37815  isbnd  37826  isdrngo1  38002  isnacs  42743  sbccomieg  42832  elmnc  43175  ismea  46495  isinv2  49064  oppcinito  49273  oppctermo  49274  oppczeroo  49275  catcsect  49436  lmdfval2  49693  cmdfval2  49694  initocmd  49707  termolmd  49708