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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  clelab  2904  elrabf  3642  elrab  3645  elrab2w  3650  sbccow  3762  sbcco  3765  sbc5ALT  3768  sbcan  3788  sbcor  3789  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcreu  3823  eldif  3909  elin  3915  elun  4100  sbccsb2  4395  2reu4  4480  eluni  4870  eliun  4955  sbcbr123  5159  elopab  5505  opelopabsb  5508  opeliunxp2  5818  inisegn0  6094  brfvopabrbr  6983  elpwun  7768  elxp5  7920  opeliunxp2f  8208  tpostpos  8244  ecdmn0  8749  brecop2  8811  elixpsn  8944  bren  8962  0sdom1dom  9216  elharval  9533  brttrcl  9692  sdom2en01  10304  isfin1-2  10387  wdomac  10530  elwina  10695  elina  10696  lterpq  10979  ltrnq  10988  elnp  10996  elnpi  10997  ltresr  11149  eluz2  12893  dfle2  13198  dflt2  13199  rexanuz2  15437  even2n  16432  isstruct2  17241  xpsfrnel2  17650  ismre  17674  isacs  17739  brssc  17903  isfunc  17953  oduclatb  18595  isipodrs  18625  issubg  19249  isnsg  19278  oppgsubm  19489  oppgsubg  19490  isslw  19735  efgrelexlema  19876  dvdsr  20503  isunit  20514  isirred  20560  isrim0  20624  issubrng  20709  opprsubrng  20721  issubrg  20733  opprsubrg  20755  islss  21118  islbs4  22045  istopon  23137  basdif0  23178  dis2ndc  23686  elmptrab  24053  isusp  24487  ismet2  24559  isphtpc  25222  elpi1  25273  iscmet  25512  bcthlem1  25552  elno  27882  elz12s  28737  dfz12s2  28753  wlkcpr  30088  isvcOLD  31060  isnv  31093  hlimi  31669  h1de2ci  32037  elunop  32353  ispcmp  34367  elmpps  36152  eldm3  36340  opelco3  36354  elima4  36355  brsset  36466  brbigcup  36475  elfix2  36481  elsingles  36495  imageval  36507  funpartlem  36521  elaltxp  36555  ellines  36732  isfne4  36959  bj-ismoore  37855  bj-idreseqb  37915  istotbnd  38519  isbnd  38530  isdrngo1  38706  isnacs  43549  sbccomieg  43634  elmnc  43977  ismea  47279  isinv2  49952  oppcinito  50161  oppctermo  50162  oppczeroo  50163  catcsect  50324  lmdfval2  50581  cmdfval2  50582  initocmd  50595  termolmd  50596