Theorem pm5.21nii 716

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  1449  elrabf  2980  sbcco  3073  sbc5  3075  sbcan  3094  sbcor  3096  sbcal  3103  sbcex2  3105  sbcel1v  3114  eldif  3229  elun  3370  elin  3412  elif  3652  rabsnif  3777  eluni  3936  eliun  4014  elopab  4398  opelopabsb  4400  opeliunxp  4828  opeliunxp2  4918  elxp4  5273  elxp5  5274  fsn2  5876  isocnv2  6012  elxp6  6397  elxp7  6398  opeliunxp2f  6503  brtpos2  6516  tpostpos  6529  ecdmn0m  6845  elixpsn  7011  bren  7024  omniwomnimkv  7501  elinp  7835  recexprlemell  7983  recexprlemelu  7984  gt0srpr  8109  ltresr  8200  eluz2  9910  elfz2  10401  infssuzex  10649  rexanuz2  11740  even2n  12624  infpn2  13330  xpsfrnel2  13650  issubg  13959  isnsg  13988  mgpplusg  14205  mgpbas  14208  ringidval  14248  issrg  14252  iscrng2  14302  opprringb  14369  isrim0  14451  opprlring  14487  issubrng  14490  issubrg  14512  rrgval  14553  opprdrng  14603  islssm  14677  islidlm  14799  2idlval  14822  2idlelb  14825  asclfval  15004  istopon  15097  ishmeo  15388  ismet2  15438  edgval  16284  istrl  16609  isclwwlk  16618  clwwlkn0  16632  isclwwlkn  16637  clwwlknonmpo  16652  clwwlknon  16653  clwwlk0on0  16655  iseupth  16671