Theorem pm5.21nii 379

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  clelab  2884  elrabf  3633  elrab  3636  elrab2w  3640  sbccow  3753  sbcco  3756  sbc5ALT  3759  sbcan  3779  sbcor  3780  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbcreu  3815  eldif  3900  elin  3906  elun  4090  sbccsb2  4372  2reu4  4459  eluni  4848  eliun  4932  sbcbr123  5133  elopab  5476  opelopabsb  5479  opeliunxp2  5787  inisegn0  6057  brfvopabrbr  6939  elpwun  7719  elxp5  7870  opeliunxp2f  8157  tpostpos  8193  ecdmn0  8693  brecop2  8755  elixpsn  8882  bren  8900  0sdom1dom  9153  elharval  9473  brttrcl  9632  sdom2en01  10222  isfin1-2  10305  wdomac  10447  elwina  10607  elina  10608  lterpq  10891  ltrnq  10900  elnp  10908  elnpi  10909  ltresr  11061  eluz2  12792  dfle2  13096  dflt2  13097  rexanuz2  15310  even2n  16309  isstruct2  17117  xpsfrnel2  17526  ismre  17550  isacs  17615  brssc  17779  isfunc  17829  oduclatb  18471  isipodrs  18501  issubg  19100  isnsg  19128  oppgsubm  19335  oppgsubg  19336  isslw  19581  efgrelexlema  19722  dvdsr  20340  isunit  20351  isirred  20397  isrim0  20460  issubrng  20526  opprsubrng  20538  issubrg  20550  opprsubrg  20572  islss  20931  islbs4  21814  istopon  22902  basdif0  22943  dis2ndc  23450  elmptrab  23817  isusp  24251  ismet2  24323  isphtpc  24986  elpi1  25037  iscmet  25276  bcthlem1  25316  elno  27634  elnoOLD  27635  elz12s  28489  dfz12s2  28505  wlkcpr  29722  isvcOLD  30675  isnv  30708  hlimi  31284  h1de2ci  31652  elunop  31968  ispcmp  34048  elmpps  35808  eldm3  35996  opelco3  36010  elima4  36011  brsset  36122  brbigcup  36131  elfix2  36137  elsingles  36151  imageval  36163  funpartlem  36177  elaltxp  36210  ellines  36387  isfne4  36575  bj-ismoore  37470  bj-idreseqb  37530  istotbnd  38143  isbnd  38154  isdrngo1  38330  isnacs  43160  sbccomieg  43245  elmnc  43588  ismea  46901  isinv2  49523  oppcinito  49732  oppctermo  49733  oppczeroo  49734  catcsect  49895  lmdfval2  50152  cmdfval2  50153  initocmd  50166  termolmd  50167