Theorem pm5.21nii 706

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  1420  elrabf  2929  sbcco  3022  sbc5  3024  sbcan  3043  sbcor  3045  sbcal  3052  sbcex2  3054  sbcel1v  3063  eldif  3177  elun  3316  elin  3358  eluni  3856  eliun  3934  elopab  4309  opelopabsb  4311  opeliunxp  4735  opeliunxp2  4823  elxp4  5176  elxp5  5177  fsn2  5764  isocnv2  5891  elxp6  6265  elxp7  6266  opeliunxp2f  6334  brtpos2  6347  tpostpos  6360  ecdmn0m  6674  elixpsn  6832  bren  6845  omniwomnimkv  7281  elinp  7600  recexprlemell  7748  recexprlemelu  7749  gt0srpr  7874  ltresr  7965  eluz2  9667  elfz2  10150  infssuzex  10389  rexanuz2  11352  even2n  12235  infpn2  12877  xpsfrnel2  13228  issubg  13559  isnsg  13588  issrg  13777  iscrng2  13827  isrim0  13973  issubrng  14011  issubrg  14033  rrgval  14074  islssm  14169  islidlm  14291  2idlval  14314  2idlelb  14317  istopon  14535  ishmeo  14826  ismet2  14876