Theorem pm5.21nii 704

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anxordi  1400  elrabf  2893  sbcco  2986  sbc5  2988  sbcan  3007  sbcor  3009  sbcal  3016  sbcex2  3018  sbcel1v  3027  eldif  3140  elun  3278  elin  3320  eluni  3814  eliun  3892  elopab  4260  opelopabsb  4262  opeliunxp  4683  opeliunxp2  4769  elxp4  5118  elxp5  5119  fsn2  5692  isocnv2  5815  elxp6  6172  elxp7  6173  opeliunxp2f  6241  brtpos2  6254  tpostpos  6267  ecdmn0m  6579  elixpsn  6737  bren  6749  omniwomnimkv  7167  elinp  7475  recexprlemell  7623  recexprlemelu  7624  gt0srpr  7749  ltresr  7840  eluz2  9536  elfz2  10017  rexanuz2  11002  even2n  11881  infssuzex  11952  infpn2  12459  xpsfrnel2  12770  issubg  13038  isnsg  13067  issrg  13153  iscrng2  13203  issubrg  13347  istopon  13598  ishmeo  13889  ismet2  13939