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  1390  elrabf  2880  sbcco  2972  sbc5  2974  sbcan  2993  sbcor  2995  sbcal  3002  sbcex2  3004  sbcel1v  3013  eldif  3125  elun  3263  elin  3305  eluni  3792  eliun  3870  elopab  4236  opelopabsb  4238  opeliunxp  4659  opeliunxp2  4744  elxp4  5091  elxp5  5092  fsn2  5659  isocnv2  5780  elxp6  6137  elxp7  6138  opeliunxp2f  6206  brtpos2  6219  tpostpos  6232  ecdmn0m  6543  elixpsn  6701  bren  6713  omniwomnimkv  7131  elinp  7415  recexprlemell  7563  recexprlemelu  7564  gt0srpr  7689  ltresr  7780  eluz2  9472  elfz2  9951  rexanuz2  10933  even2n  11811  infssuzex  11882  infpn2  12389  istopon  12661  ishmeo  12954  ismet2  13004