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  2884  elrabf  3690  elrab  3694  elrab2w  3698  sbccow  3813  sbcco  3816  sbc5ALT  3819  sbcan  3843  sbcor  3844  sbcal  3854  sbcex2  3855  sbcel1v  3861  sbcreu  3884  eldif  3972  elin  3978  elun  4162  sbccsb2  4442  2reu4  4528  eluni  4914  eliun  4999  sbcbr123  5201  elopab  5536  opelopabsb  5539  opeliunxp2  5851  inisegn0  6118  brfvopabrbr  7012  elpwun  7787  elxp5  7945  opeliunxp2f  8233  tpostpos  8269  ecdmn0  8792  brecop2  8849  elixpsn  8975  bren  8993  0sdom1dom  9271  elharval  9598  brttrcl  9750  sdom2en01  10339  isfin1-2  10422  wdomac  10564  elwina  10723  elina  10724  lterpq  11007  ltrnq  11016  elnp  11024  elnpi  11025  ltresr  11177  eluz2  12881  dfle2  13185  dflt2  13186  rexanuz2  15384  even2n  16375  isstruct2  17182  xpsfrnel2  17610  ismre  17634  isacs  17695  brssc  17861  isfunc  17914  oduclatb  18564  isipodrs  18594  issubg  19156  isnsg  19185  oppgsubm  19395  oppgsubg  19396  isslw  19640  efgrelexlema  19781  dvdsr  20378  isunit  20389  isirred  20435  isrim0  20499  issubrng  20563  opprsubrng  20575  issubrg  20587  opprsubrg  20609  islss  20949  islbs4  21869  istopon  22933  basdif0  22975  dis2ndc  23483  elmptrab  23850  isusp  24285  ismet2  24358  isphtpc  25039  elpi1  25091  iscmet  25331  bcthlem1  25371  elno  27704  elnoOLD  27705  elzs12  28435  wlkcpr  29661  isvcOLD  30607  isnv  30640  hlimi  31216  h1de2ci  31584  elunop  31900  ispcmp  33817  elmpps  35557  eldm3  35740  opelco3  35755  elima4  35756  brsset  35870  brbigcup  35879  elfix2  35885  elsingles  35899  imageval  35911  funpartlem  35923  elaltxp  35956  ellines  36133  isfne4  36322  bj-ismoore  37087  bj-idreseqb  37145  istotbnd  37755  isbnd  37766  isdrngo1  37942  isnacs  42691  sbccomieg  42780  elmnc  43124  ismea  46406