Theorem pm5.21nii 381

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 380	. 2 ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒))
5	1, 4	pm2.61i 184	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  2913  elrabf  3656  elrab  3659  elrab2w  3664  sbccow  3776  sbcco  3779  sbc5ALT  3782  sbcan  3802  sbcor  3803  sbcal  3812  sbcex2  3813  sbcel1v  3818  sbcreu  3838  eldif  3923  elin  3929  elun  4115  sbccsb2  4408  2reu4  4490  eluni  4879  eliun  4964  sbcbr123  5169  elopab  5512  opelopabsb  5515  opeliunxp2  5825  inisegn0  6101  brfvopabrbr  6987  elpwun  7768  elxp5  7920  opeliunxp2f  8206  tpostpos  8242  ecdmn0  8747  brecop2  8809  elixpsn  8935  bren  8953  0sdom1dom  9206  elharval  9523  brttrcl  9682  sdom2en01  10286  isfin1-2  10369  wdomac  10511  elwina  10671  elina  10672  lterpq  10955  ltrnq  10964  elnp  10972  elnpi  10973  ltresr  11125  eluz2  12868  dfle2  13172  dflt2  13173  rexanuz2  15401  even2n  16400  isstruct2  17209  xpsfrnel2  17618  ismre  17642  isacs  17707  brssc  17871  isfunc  17921  oduclatb  18563  isipodrs  18593  issubg  19192  isnsg  19221  oppgsubm  19432  oppgsubg  19433  isslw  19678  efgrelexlema  19819  dvdsr  20444  isunit  20455  isirred  20501  isrim0  20564  issubrng  20632  opprsubrng  20644  issubrg  20656  opprsubrg  20678  islss  21033  islbs4  21951  istopon  23038  basdif0  23079  dis2ndc  23586  elmptrab  23953  isusp  24387  ismet2  24459  isphtpc  25122  elpi1  25173  iscmet  25412  bcthlem1  25452  elno  27776  elz12s  28631  dfz12s2  28647  wlkcpr  29919  isvcOLD  30872  isnv  30905  hlimi  31481  h1de2ci  31849  elunop  32165  ispcmp  34192  elmpps  35998  eldm3  36186  opelco3  36200  elima4  36201  brsset  36312  brbigcup  36321  elfix2  36327  elsingles  36341  imageval  36353  funpartlem  36367  elaltxp  36400  ellines  36577  isfne4  36774  bj-ismoore  37669  bj-idreseqb  37729  istotbnd  38342  isbnd  38353  isdrngo1  38529  isnacs  43361  sbccomieg  43446  elmnc  43789  ismea  47091  isinv2  49723  oppcinito  49932  oppctermo  49933  oppczeroo  49934  catcsect  50095  lmdfval2  50352  cmdfval2  50353  initocmd  50366  termolmd  50367