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  2880  elrabf  3667  elrab  3671  elrab2w  3675  sbccow  3788  sbcco  3791  sbc5ALT  3794  sbcan  3815  sbcor  3816  sbcal  3825  sbcex2  3826  sbcel1v  3831  sbcreu  3851  eldif  3936  elin  3942  elun  4128  sbccsb2  4412  2reu4  4498  eluni  4886  eliun  4971  sbcbr123  5173  elopab  5502  opelopabsb  5505  opeliunxp2  5818  inisegn0  6085  brfvopabrbr  6983  elpwun  7763  elxp5  7919  opeliunxp2f  8209  tpostpos  8245  ecdmn0  8768  brecop2  8825  elixpsn  8951  bren  8969  0sdom1dom  9246  elharval  9575  brttrcl  9727  sdom2en01  10316  isfin1-2  10399  wdomac  10541  elwina  10700  elina  10701  lterpq  10984  ltrnq  10993  elnp  11001  elnpi  11002  ltresr  11154  eluz2  12858  dfle2  13163  dflt2  13164  rexanuz2  15368  even2n  16361  isstruct2  17168  xpsfrnel2  17578  ismre  17602  isacs  17663  brssc  17827  isfunc  17877  oduclatb  18517  isipodrs  18547  issubg  19109  isnsg  19138  oppgsubm  19345  oppgsubg  19346  isslw  19589  efgrelexlema  19730  dvdsr  20322  isunit  20333  isirred  20379  isrim0  20443  issubrng  20507  opprsubrng  20519  issubrg  20531  opprsubrg  20553  islss  20891  islbs4  21792  istopon  22850  basdif0  22891  dis2ndc  23398  elmptrab  23765  isusp  24200  ismet2  24272  isphtpc  24944  elpi1  24996  iscmet  25236  bcthlem1  25276  elno  27609  elnoOLD  27610  elzs12  28389  wlkcpr  29609  isvcOLD  30560  isnv  30593  hlimi  31169  h1de2ci  31537  elunop  31853  ispcmp  33888  elmpps  35595  eldm3  35778  opelco3  35792  elima4  35793  brsset  35907  brbigcup  35916  elfix2  35922  elsingles  35936  imageval  35948  funpartlem  35960  elaltxp  35993  ellines  36170  isfne4  36358  bj-ismoore  37123  bj-idreseqb  37181  istotbnd  37793  isbnd  37804  isdrngo1  37980  isnacs  42727  sbccomieg  42816  elmnc  43160  ismea  46480  oppcinito  49152  oppctermo  49153  oppczeroo  49154  lmdfval2  49527  cmdfval2  49528