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  2877  elrabf  3678  elrab  3682  sbccow  3799  sbcco  3802  sbc5ALT  3805  sbcan  3828  sbcor  3829  sbcal  3840  sbcex2  3841  sbcel1v  3847  sbcreu  3869  eldif  3957  elin  3963  elun  4147  sbccsb2  4433  2reu4  4525  elpr2OLD  4653  eluni  4910  eliun  5000  sbcbr123  5201  elopab  5526  opelopabsb  5529  opeliunxp2  5837  inisegn0  6096  brfvopabrbr  6994  elpwun  7758  elxp5  7916  opeliunxp2f  8197  tpostpos  8233  ecdmn0  8752  brecop2  8807  elixpsn  8933  bren  8951  brenOLD  8952  0sdom1dom  9240  elharval  9558  brttrcl  9710  sdom2en01  10299  isfin1-2  10382  wdomac  10524  elwina  10683  elina  10684  lterpq  10967  ltrnq  10976  elnp  10984  elnpi  10985  ltresr  11137  eluz2  12832  dfle2  13130  dflt2  13131  rexanuz2  15300  even2n  16289  isstruct2  17086  xpsfrnel2  17514  ismre  17538  isacs  17599  brssc  17765  isfunc  17818  oduclatb  18464  isipodrs  18494  issubg  19042  isnsg  19071  oppgsubm  19270  oppgsubg  19271  isslw  19517  efgrelexlema  19658  dvdsr  20253  isunit  20264  isirred  20310  isrim0  20374  issubrng  20435  opprsubrng  20447  issubrg  20461  opprsubrg  20483  islss  20689  islbs4  21606  istopon  22634  basdif0  22676  dis2ndc  23184  elmptrab  23551  isusp  23986  ismet2  24059  isphtpc  24740  elpi1  24792  iscmet  25032  bcthlem1  25072  elno  27385  wlkcpr  29153  isvcOLD  30099  isnv  30132  hlimi  30708  h1de2ci  31076  elunop  31392  ispcmp  33135  elmpps  34862  eldm3  35035  opelco3  35050  elima4  35051  brsset  35165  brbigcup  35174  elfix2  35180  elsingles  35194  imageval  35206  funpartlem  35218  elaltxp  35251  ellines  35428  isfne4  35528  bj-ismoore  36289  bj-idreseqb  36347  istotbnd  36940  isbnd  36951  isdrngo1  37127  elrab2w  41712  isnacs  41744  sbccomieg  41833  elmnc  42180  ismea  45465