Theorem pm5.21nii 699

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  1395  elrabf  2884  sbcco  2976  sbc5  2978  sbcan  2997  sbcor  2999  sbcal  3006  sbcex2  3008  sbcel1v  3017  eldif  3130  elun  3268  elin  3310  eluni  3799  eliun  3877  elopab  4243  opelopabsb  4245  opeliunxp  4666  opeliunxp2  4751  elxp4  5098  elxp5  5099  fsn2  5670  isocnv2  5791  elxp6  6148  elxp7  6149  opeliunxp2f  6217  brtpos2  6230  tpostpos  6243  ecdmn0m  6555  elixpsn  6713  bren  6725  omniwomnimkv  7143  elinp  7436  recexprlemell  7584  recexprlemelu  7585  gt0srpr  7710  ltresr  7801  eluz2  9493  elfz2  9972  rexanuz2  10955  even2n  11833  infssuzex  11904  infpn2  12411  istopon  12805  ishmeo  13098  ismet2  13148