Theorem pm5.21nii 380

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  clelab  2905  elrabf  3646  elrab  3649  elrab2w  3653  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3791  sbcor  3792  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbcreu  3827  eldif  3912  elin  3918  elun  4104  sbccsb2  4388  2reu4  4475  eluni  4865  eliun  4950  sbcbr123  5151  elopab  5494  opelopabsb  5497  opeliunxp2  5806  inisegn0  6082  brfvopabrbr  6966  elpwun  7746  elxp5  7898  opeliunxp2f  8183  tpostpos  8219  ecdmn0  8724  brecop2  8786  elixpsn  8912  bren  8930  0sdom1dom  9183  elharval  9502  brttrcl  9661  sdom2en01  10252  isfin1-2  10335  wdomac  10477  elwina  10637  elina  10638  lterpq  10921  ltrnq  10930  elnp  10938  elnpi  10939  ltresr  11091  eluz2  12838  dfle2  13142  dflt2  13143  rexanuz2  15367  even2n  16366  isstruct2  17175  xpsfrnel2  17584  ismre  17608  isacs  17673  brssc  17837  isfunc  17887  oduclatb  18529  isipodrs  18559  issubg  19158  isnsg  19186  oppgsubm  19392  oppgsubg  19393  isslw  19638  efgrelexlema  19779  dvdsr  20397  isunit  20408  isirred  20454  isrim0  20517  issubrng  20583  opprsubrng  20595  issubrg  20607  opprsubrg  20629  islss  20988  islbs4  21871  istopon  22959  basdif0  23000  dis2ndc  23507  elmptrab  23874  isusp  24308  ismet2  24380  isphtpc  25043  elpi1  25094  iscmet  25333  bcthlem1  25373  elno  27697  elz12s  28552  dfz12s2  28568  wlkcpr  29785  isvcOLD  30738  isnv  30771  hlimi  31347  h1de2ci  31715  elunop  32031  ispcmp  34114  elmpps  35883  eldm3  36071  opelco3  36085  elima4  36086  brsset  36197  brbigcup  36206  elfix2  36212  elsingles  36226  imageval  36238  funpartlem  36252  elaltxp  36285  ellines  36462  isfne4  36660  bj-ismoore  37555  bj-idreseqb  37615  istotbnd  38228  isbnd  38239  isdrngo1  38415  isnacs  43245  sbccomieg  43330  elmnc  43673  ismea  46985  isinv2  49607  oppcinito  49816  oppctermo  49817  oppczeroo  49818  catcsect  49979  lmdfval2  50236  cmdfval2  50237  initocmd  50250  termolmd  50251