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  3891  eliun  3969  elopab  4346  opelopabsb  4348  opeliunxp  4774  opeliunxp2  4862  elxp4  5216  elxp5  5217  fsn2  5811  isocnv2  5942  elxp6  6321  elxp7  6322  opeliunxp2f  6390  brtpos2  6403  tpostpos  6416  ecdmn0m  6732  elixpsn  6890  bren  6903  omniwomnimkv  7342  elinp  7669  recexprlemell  7817  recexprlemelu  7818  gt0srpr  7943  ltresr  8034  eluz2  9736  elfz2  10219  infssuzex  10461  rexanuz2  11510  even2n  12393  infpn2  13035  xpsfrnel2  13387  issubg  13718  isnsg  13747  issrg  13936  iscrng2  13986  isrim0  14133  issubrng  14171  issubrg  14193  rrgval  14234  islssm  14329  islidlm  14451  2idlval  14474  2idlelb  14477  istopon  14695  ishmeo  14986  ismet2  15036  istrl  16104