Theorem pm5.21nii 377

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  clelab  2871  elrabf  3675  elrab  3679  sbccow  3796  sbcco  3799  sbc5ALT  3802  sbcan  3826  sbcor  3827  sbcal  3837  sbcex2  3838  sbcel1v  3844  sbcreu  3866  eldif  3954  elin  3960  elun  4145  sbccsb2  4436  2reu4  4528  eluni  4912  eliun  5001  sbcbr123  5203  elopab  5529  opelopabsb  5532  opeliunxp2  5841  inisegn0  6103  brfvopabrbr  7001  elpwun  7772  elxp5  7931  opeliunxp2f  8216  tpostpos  8252  ecdmn0  8773  brecop2  8830  elixpsn  8956  bren  8974  brenOLD  8975  0sdom1dom  9266  elharval  9591  brttrcl  9743  sdom2en01  10332  isfin1-2  10415  wdomac  10557  elwina  10716  elina  10717  lterpq  11000  ltrnq  11009  elnp  11017  elnpi  11018  ltresr  11170  eluz2  12866  dfle2  13166  dflt2  13167  rexanuz2  15340  even2n  16330  isstruct2  17137  xpsfrnel2  17565  ismre  17589  isacs  17650  brssc  17816  isfunc  17869  oduclatb  18518  isipodrs  18548  issubg  19106  isnsg  19135  oppgsubm  19345  oppgsubg  19346  isslw  19592  efgrelexlema  19733  dvdsr  20330  isunit  20341  isirred  20387  isrim0  20451  issubrng  20513  opprsubrng  20525  issubrg  20539  opprsubrg  20561  islss  20847  islbs4  21800  istopon  22875  basdif0  22917  dis2ndc  23425  elmptrab  23792  isusp  24227  ismet2  24300  isphtpc  24981  elpi1  25033  iscmet  25273  bcthlem1  25313  elno  27644  elnoOLD  27645  wlkcpr  29535  isvcOLD  30481  isnv  30514  hlimi  31090  h1de2ci  31458  elunop  31774  ispcmp  33609  elmpps  35334  eldm3  35506  opelco3  35521  elima4  35522  brsset  35636  brbigcup  35645  elfix2  35651  elsingles  35665  imageval  35677  funpartlem  35689  elaltxp  35722  ellines  35899  isfne4  35975  bj-ismoore  36735  bj-idreseqb  36793  istotbnd  37393  isbnd  37404  isdrngo1  37580  elrab2w  42232  isnacs  42271  sbccomieg  42360  elmnc  42707  ismea  45982