Theorem pm5.21nii 368

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  elrabf  3360  sbcco  3458  sbc5  3460  sbcan  3478  sbcor  3479  sbcal  3485  sbcex2  3486  sbcel1v  3495  sbcreu  3515  eldif  3584  elun  3753  elin  3796  sbccsb2  4005  elpr2  4199  eluni  4439  eliun  4524  sbcbr123  4706  elopab  4983  opelopabsb  4985  opeliunxp2  5260  inisegn0  5497  brfvopabrbr  6279  elpwun  6977  elxp5  7111  opeliunxp2f  7336  tpostpos  7372  ecdmn0  7789  brecop2  7841  elixpsn  7947  bren  7964  elharval  8468  sdom2en01  9124  isfin1-2  9207  wdomac  9349  elwina  9508  elina  9509  lterpq  9792  ltrnq  9801  elnp  9809  elnpi  9810  ltresr  9961  eluz2  11693  dfle2  11980  dflt2  11981  rexanuz2  14089  even2n  15066  isstruct2  15867  xpsfrnel2  16225  ismre  16250  isacs  16312  brssc  16474  isfunc  16524  oduclatb  17144  isipodrs  17161  issubg  17594  isnsg  17623  oppgsubm  17792  oppgsubg  17793  isslw  18023  efgrelexlema  18162  dvdsr  18646  isunit  18657  isirred  18699  issubrg  18780  opprsubrg  18801  islss  18935  islbs4  20171  istopon  20717  basdif0  20757  dis2ndc  21263  elmptrab  21630  isusp  22065  ismet2  22138  isphtpc  22793  elpi1  22845  iscmet  23082  bcthlem1  23121  wlkcpr  26524  isclwwlksng  26888  frgrusgrfrcond  27123  isvcOLD  27434  isnv  27467  hlimi  28045  h1de2ci  28415  elunop  28731  ispcmp  29924  elmpps  31470  eldm3  31651  opelco3  31678  elima4  31679  elno  31799  brsset  31996  brbigcup  32005  elfix2  32011  elsingles  32025  imageval  32037  funpartlem  32049  elaltxp  32082  ellines  32259  isfne4  32335  istotbnd  33568  isbnd  33579  isdrngo1  33755  isnacs  37267  sbccomieg  37357  elmnc  37706  2reu4  41190