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  2874  elrabf  3658  elrab  3662  elrab2w  3666  sbccow  3779  sbcco  3782  sbc5ALT  3785  sbcan  3806  sbcor  3807  sbcal  3816  sbcex2  3817  sbcel1v  3822  sbcreu  3842  eldif  3927  elin  3933  elun  4119  sbccsb2  4403  2reu4  4489  eluni  4877  eliun  4962  sbcbr123  5164  elopab  5490  opelopabsb  5493  opeliunxp2  5805  inisegn0  6072  brfvopabrbr  6968  elpwun  7748  elxp5  7902  opeliunxp2f  8192  tpostpos  8228  ecdmn0  8726  brecop2  8787  elixpsn  8913  bren  8931  0sdom1dom  9192  elharval  9521  brttrcl  9673  sdom2en01  10262  isfin1-2  10345  wdomac  10487  elwina  10646  elina  10647  lterpq  10930  ltrnq  10939  elnp  10947  elnpi  10948  ltresr  11100  eluz2  12806  dfle2  13114  dflt2  13115  rexanuz2  15323  even2n  16319  isstruct2  17126  xpsfrnel2  17534  ismre  17558  isacs  17619  brssc  17783  isfunc  17833  oduclatb  18473  isipodrs  18503  issubg  19065  isnsg  19094  oppgsubm  19301  oppgsubg  19302  isslw  19545  efgrelexlema  19686  dvdsr  20278  isunit  20289  isirred  20335  isrim0  20399  issubrng  20463  opprsubrng  20475  issubrg  20487  opprsubrg  20509  islss  20847  islbs4  21748  istopon  22806  basdif0  22847  dis2ndc  23354  elmptrab  23721  isusp  24156  ismet2  24228  isphtpc  24900  elpi1  24952  iscmet  25191  bcthlem1  25231  elno  27564  elnoOLD  27565  elzs12  28344  wlkcpr  29564  isvcOLD  30515  isnv  30548  hlimi  31124  h1de2ci  31492  elunop  31808  ispcmp  33854  elmpps  35567  eldm3  35755  opelco3  35769  elima4  35770  brsset  35884  brbigcup  35893  elfix2  35899  elsingles  35913  imageval  35925  funpartlem  35937  elaltxp  35970  ellines  36147  isfne4  36335  bj-ismoore  37100  bj-idreseqb  37158  istotbnd  37770  isbnd  37781  isdrngo1  37957  isnacs  42699  sbccomieg  42788  elmnc  43132  ismea  46456  isinv2  49019  oppcinito  49228  oppctermo  49229  oppczeroo  49230  catcsect  49391  lmdfval2  49648  cmdfval2  49649  initocmd  49662  termolmd  49663