Theorem pm5.21nii 652

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anxordi  1331  elrabf  2747  sbcco  2836  sbc5  2838  sbcan  2856  sbcor  2858  sbcal  2865  sbcex2  2867  sbcel1v  2876  eldif  2982  elun  3113  elin  3155  eluni  3604  eliun  3682  elopab  4013  opelopabsb  4015  opeliunxp  4413  opeliunxp2  4494  elxp4  4828  elxp5  4829  fsn2  5358  isocnv2  5472  elxp6  5816  elxp7  5817  brtpos2  5889  tpostpos  5902  ecdmn0m  6171  bren  6251  elinp  6664  recexprlemell  6812  recexprlemelu  6813  gt0srpr  6925  ltresr  7007  eluz2  8625  elfz2  9036  rexanuz2  9877  even2n  10273  infssuzex  10345