Theorem pm5.21nii 694

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anxordi  1379  elrabf  2842  sbcco  2934  sbc5  2936  sbcan  2955  sbcor  2957  sbcal  2964  sbcex2  2966  sbcel1v  2975  eldif  3085  elun  3222  elin  3264  eluni  3747  eliun  3825  elopab  4188  opelopabsb  4190  opeliunxp  4602  opeliunxp2  4687  elxp4  5034  elxp5  5035  fsn2  5602  isocnv2  5721  elxp6  6075  elxp7  6076  opeliunxp2f  6143  brtpos2  6156  tpostpos  6169  ecdmn0m  6479  elixpsn  6637  bren  6649  omniwomnimkv  7049  elinp  7306  recexprlemell  7454  recexprlemelu  7455  gt0srpr  7580  ltresr  7671  eluz2  9356  elfz2  9828  rexanuz2  10795  even2n  11607  infssuzex  11678  istopon  12219  ishmeo  12512  ismet2  12562