Theorem pm5.21nii 658

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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anxordi  1343  elrabf  2783  sbcco  2875  sbc5  2877  sbcan  2895  sbcor  2897  sbcal  2904  sbcex2  2906  sbcel1v  2915  eldif  3022  elun  3156  elin  3198  eluni  3678  eliun  3756  elopab  4109  opelopabsb  4111  opeliunxp  4522  opeliunxp2  4607  elxp4  4952  elxp5  4953  fsn2  5510  isocnv2  5629  elxp6  5978  elxp7  5979  opeliunxp2f  6041  brtpos2  6054  tpostpos  6067  ecdmn0m  6374  elixpsn  6532  bren  6544  elinp  7130  recexprlemell  7278  recexprlemelu  7279  gt0srpr  7391  ltresr  7473  eluz2  9124  elfz2  9580  rexanuz2  10539  even2n  11301  infssuzex  11372  istopon  11864  ismet2  12140