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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3778  eluni  3938  eliun  4016  elopab  4402  opelopabsb  4404  opeliunxp  4832  opeliunxp2  4922  elxp4  5278  elxp5  5279  fsn2  5885  isocnv2  6021  elxp6  6407  elxp7  6408  opeliunxp2f  6513  brtpos2  6526  tpostpos  6539  ecdmn0m  6855  elixpsn  7022  bren  7035  omniwomnimkv  7514  elinp  7848  recexprlemell  7996  recexprlemelu  7997  gt0srpr  8122  ltresr  8213  eluz2  9944  elfz2  10436  infssuzex  10684  rexanuz2  11780  even2n  12667  infpn2  13406  xpsfrnel2  13727  issubg  14036  isnsg  14065  cntrval  14152  mgpplusg  14330  mgpbas  14333  ringidval  14373  issrg  14377  iscrng2  14427  opprringb  14496  isrim0  14578  opprlring  14614  issubrng  14617  issubrg  14639  rrgval  14680  opprdrng  14730  islssm  14804  islidlm  14926  2idlval  14949  2idlelb  14952  asclfval  15131  istopon  15251  ishmeo  15542  ismet2  15592  edgval  16518  istrl  16843  isclwwlk  16852  clwwlkn0  16866  isclwwlkn  16871  clwwlknonmpo  16886  clwwlknon  16887  clwwlk0on0  16889  iseupth  16905