Theorem pm5.21nii 712

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  1445  elrabf  2970  sbcco  3063  sbc5  3065  sbcan  3084  sbcor  3086  sbcal  3093  sbcex2  3095  sbcel1v  3104  eldif  3219  elun  3359  elin  3401  elif  3633  rabsnif  3757  eluni  3916  eliun  3994  elopab  4375  opelopabsb  4377  opeliunxp  4804  opeliunxp2  4894  elxp4  5249  elxp5  5250  fsn2  5850  isocnv2  5984  elxp6  6362  elxp7  6363  opeliunxp2f  6468  brtpos2  6481  tpostpos  6494  ecdmn0m  6810  elixpsn  6969  bren  6982  omniwomnimkv  7457  elinp  7788  recexprlemell  7936  recexprlemelu  7937  gt0srpr  8062  ltresr  8153  eluz2  9858  elfz2  10348  infssuzex  10592  rexanuz2  11672  even2n  12556  infpn2  13199  xpsfrnel2  13551  issubg  13882  isnsg  13911  issrg  14101  iscrng2  14151  isrim0  14298  issubrng  14336  issubrg  14358  rrgval  14399  islssm  14497  islidlm  14619  2idlval  14642  2idlelb  14645  istopon  14870  ishmeo  15161  ismet2  15211  edgval  16047  istrl  16372  isclwwlk  16381  clwwlkn0  16395  isclwwlkn  16400  clwwlknonmpo  16415  clwwlknon  16416  clwwlk0on0  16418  iseupth  16434