Theorem pm5.21nii 709

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  1442  elrabf  2957  sbcco  3050  sbc5  3052  sbcan  3071  sbcor  3073  sbcal  3080  sbcex2  3082  sbcel1v  3091  eldif  3206  elun  3345  elin  3387  elif  3614  eluni  3890  eliun  3968  elopab  4345  opelopabsb  4347  opeliunxp  4771  opeliunxp2  4859  elxp4  5212  elxp5  5213  fsn2  5802  isocnv2  5929  elxp6  6305  elxp7  6306  opeliunxp2f  6374  brtpos2  6387  tpostpos  6400  ecdmn0m  6714  elixpsn  6872  bren  6885  omniwomnimkv  7322  elinp  7649  recexprlemell  7797  recexprlemelu  7798  gt0srpr  7923  ltresr  8014  eluz2  9716  elfz2  10199  infssuzex  10440  rexanuz2  11488  even2n  12371  infpn2  13013  xpsfrnel2  13365  issubg  13696  isnsg  13725  issrg  13914  iscrng2  13964  isrim0  14110  issubrng  14148  issubrg  14170  rrgval  14211  islssm  14306  islidlm  14428  2idlval  14451  2idlelb  14454  istopon  14672  ishmeo  14963  ismet2  15013