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  4347  opelopabsb  4349  opeliunxp  4776  opeliunxp2  4865  elxp4  5219  elxp5  5220  fsn2  5814  isocnv2  5945  elxp6  6324  elxp7  6325  opeliunxp2f  6395  brtpos2  6408  tpostpos  6421  ecdmn0m  6737  elixpsn  6895  bren  6908  omniwomnimkv  7350  elinp  7677  recexprlemell  7825  recexprlemelu  7826  gt0srpr  7951  ltresr  8042  eluz2  9744  elfz2  10228  infssuzex  10470  rexanuz2  11523  even2n  12406  infpn2  13048  xpsfrnel2  13400  issubg  13731  isnsg  13760  issrg  13949  iscrng2  13999  isrim0  14146  issubrng  14184  issubrg  14206  rrgval  14247  islssm  14342  islidlm  14464  2idlval  14487  2idlelb  14490  istopon  14708  ishmeo  14999  ismet2  15049  istrl  16155  isclwwlk  16163  clwwlkn0  16177