Theorem pm5.21nii 383

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  clelab  2880  elrabf  3598  elrab  3602  sbccow  3717  sbcco  3720  sbc5ALT  3723  sbcan  3746  sbcor  3747  sbcal  3759  sbcex2  3760  sbcel1v  3766  sbcreu  3788  eldif  3876  elin  3882  elun  4063  sbccsb2  4349  2reu4  4438  elpr2OLD  4567  eluni  4822  eliun  4908  sbcbr123  5107  elopab  5408  opelopabsb  5411  opeliunxp2  5707  inisegn0  5966  brfvopabrbr  6815  elpwun  7554  elxp5  7701  opeliunxp2f  7952  tpostpos  7988  ecdmn0  8438  brecop2  8493  elixpsn  8618  bren  8636  brenOLD  8637  elharval  9177  sdom2en01  9916  isfin1-2  9999  wdomac  10141  elwina  10300  elina  10301  lterpq  10584  ltrnq  10593  elnp  10601  elnpi  10602  ltresr  10754  eluz2  12444  dfle2  12737  dflt2  12738  rexanuz2  14913  even2n  15903  isstruct2  16702  xpsfrnel2  17069  ismre  17093  isacs  17154  brssc  17319  isfunc  17370  oduclatb  18013  isipodrs  18043  issubg  18543  isnsg  18571  oppgsubm  18754  oppgsubg  18755  isslw  18997  efgrelexlema  19139  dvdsr  19664  isunit  19675  isirred  19717  issubrg  19800  opprsubrg  19821  islss  19971  islbs4  20794  istopon  21809  basdif0  21850  dis2ndc  22357  elmptrab  22724  isusp  23159  ismet2  23231  isphtpc  23891  elpi1  23942  iscmet  24181  bcthlem1  24221  wlkcpr  27716  isvcOLD  28660  isnv  28693  hlimi  29269  h1de2ci  29637  elunop  29953  ispcmp  31521  elmpps  33248  eldm3  33447  opelco3  33468  elima4  33469  brttrcl  33512  elno  33586  brsset  33928  brbigcup  33937  elfix2  33943  elsingles  33957  imageval  33969  funpartlem  33981  elaltxp  34014  ellines  34191  isfne4  34266  bj-ismoore  35011  bj-idreseqb  35069  istotbnd  35664  isbnd  35675  isdrngo1  35851  elrab2w  39889  isnacs  40229  sbccomieg  40318  elmnc  40664  ismea  43664