Theorem pm5.21nii 716

Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.)

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.21ni.1	. . . 4 ⊢ (𝜑 → 𝜓)
2		pm5.21nii.3	. . . 4 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
3	1, 2	syl 14	. . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜒))
4	3	ibi 176	. 2 ⊢ (𝜑 → 𝜒)
5		pm5.21ni.2	. . . 4 ⊢ (𝜒 → 𝜓)
6	5, 2	syl 14	. . 3 ⊢ (𝜒 → (𝜑 ↔ 𝜒))
7	6	ibir 177	. 2 ⊢ (𝜒 → 𝜑)
8	4, 7	impbii 126	1 ⊢ (𝜑 ↔ 𝜒)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anxordi  1449  elrabf  2980  sbcco  3073  sbc5  3075  sbcan  3094  sbcor  3096  sbcal  3103  sbcex2  3105  sbcel1v  3114  eldif  3229  elun  3370  elin  3412  elif  3652  rabsnif  3778  eluni  3938  eliun  4016  elopab  4402  opelopabsb  4404  opeliunxp  4832  opeliunxp2  4922  elxp4  5278  elxp5  5279  fsn2  5885  isocnv2  6021  elxp6  6407  elxp7  6408  opeliunxp2f  6514  brtpos2  6527  tpostpos  6540  ecdmn0m  6856  elixpsn  7023  bren  7036  omniwomnimkv  7514  elinp  7848  recexprlemell  7996  recexprlemelu  7997  gt0srpr  8122  ltresr  8213  eluz2  9943  elfz2  10435  infssuzex  10683  rexanuz2  11779  even2n  12666  infpn2  13405  xpsfrnel2  13726  issubg  14035  isnsg  14064  cntrval  14151  mgpplusg  14329  mgpbas  14332  ringidval  14372  issrg  14376  iscrng2  14426  opprringb  14495  isrim0  14577  opprlring  14613  issubrng  14616  issubrg  14638  rrgval  14679  opprdrng  14729  islssm  14803  islidlm  14925  2idlval  14948  2idlelb  14951  asclfval  15130  mplbas  15235  istopon  15272  ishmeo  15563  ismet2  15613  edgval  16539  istrl  16864  isclwwlk  16873  clwwlkn0  16887  isclwwlkn  16892  clwwlknonmpo  16907  clwwlknon  16908  clwwlk0on0  16910  iseupth  16926