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  2890  elrabf  3704  elrab  3708  elrab2w  3712  sbccow  3827  sbcco  3830  sbc5ALT  3833  sbcan  3857  sbcor  3858  sbcal  3868  sbcex2  3869  sbcel1v  3875  sbcreu  3898  eldif  3986  elin  3992  elun  4176  sbccsb2  4460  2reu4  4546  eluni  4934  eliun  5019  sbcbr123  5220  elopab  5546  opelopabsb  5549  opeliunxp2  5863  inisegn0  6128  brfvopabrbr  7026  elpwun  7804  elxp5  7963  opeliunxp2f  8251  tpostpos  8287  ecdmn0  8812  brecop2  8869  elixpsn  8995  bren  9013  brenOLD  9014  0sdom1dom  9301  elharval  9630  brttrcl  9782  sdom2en01  10371  isfin1-2  10454  wdomac  10596  elwina  10755  elina  10756  lterpq  11039  ltrnq  11048  elnp  11056  elnpi  11057  ltresr  11209  eluz2  12909  dfle2  13209  dflt2  13210  rexanuz2  15398  even2n  16390  isstruct2  17196  xpsfrnel2  17624  ismre  17648  isacs  17709  brssc  17875  isfunc  17928  oduclatb  18577  isipodrs  18607  issubg  19166  isnsg  19195  oppgsubm  19405  oppgsubg  19406  isslw  19650  efgrelexlema  19791  dvdsr  20388  isunit  20399  isirred  20445  isrim0  20509  issubrng  20573  opprsubrng  20585  issubrg  20599  opprsubrg  20621  islss  20955  islbs4  21875  istopon  22939  basdif0  22981  dis2ndc  23489  elmptrab  23856  isusp  24291  ismet2  24364  isphtpc  25045  elpi1  25097  iscmet  25337  bcthlem1  25377  elno  27708  elnoOLD  27709  elzs12  28439  wlkcpr  29665  isvcOLD  30611  isnv  30644  hlimi  31220  h1de2ci  31588  elunop  31904  ispcmp  33803  elmpps  35541  eldm3  35723  opelco3  35738  elima4  35739  brsset  35853  brbigcup  35862  elfix2  35868  elsingles  35882  imageval  35894  funpartlem  35906  elaltxp  35939  ellines  36116  isfne4  36306  bj-ismoore  37071  bj-idreseqb  37129  istotbnd  37729  isbnd  37740  isdrngo1  37916  isnacs  42660  sbccomieg  42749  elmnc  43093  ismea  46372