Theorem pm5.21nii 693

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  1378  elrabf  2838  sbcco  2930  sbc5  2932  sbcan  2951  sbcor  2953  sbcal  2960  sbcex2  2962  sbcel1v  2971  eldif  3080  elun  3217  elin  3259  eluni  3739  eliun  3817  elopab  4180  opelopabsb  4182  opeliunxp  4594  opeliunxp2  4679  elxp4  5026  elxp5  5027  fsn2  5594  isocnv2  5713  elxp6  6067  elxp7  6068  opeliunxp2f  6135  brtpos2  6148  tpostpos  6161  ecdmn0m  6471  elixpsn  6629  bren  6641  elinp  7282  recexprlemell  7430  recexprlemelu  7431  gt0srpr  7556  ltresr  7647  eluz2  9332  elfz2  9797  rexanuz2  10763  even2n  11571  infssuzex  11642  istopon  12180  ishmeo  12473  ismet2  12523