Theorem pm5.21nii 711

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  1444  elrabf  2960  sbcco  3053  sbc5  3055  sbcan  3074  sbcor  3076  sbcal  3083  sbcex2  3085  sbcel1v  3094  eldif  3209  elun  3348  elin  3390  elif  3617  rabsnif  3738  eluni  3896  eliun  3974  elopab  4352  opelopabsb  4354  opeliunxp  4781  opeliunxp2  4870  elxp4  5224  elxp5  5225  fsn2  5821  isocnv2  5953  elxp6  6332  elxp7  6333  opeliunxp2f  6404  brtpos2  6417  tpostpos  6430  ecdmn0m  6746  elixpsn  6904  bren  6917  omniwomnimkv  7366  elinp  7694  recexprlemell  7842  recexprlemelu  7843  gt0srpr  7968  ltresr  8059  eluz2  9761  elfz2  10250  infssuzex  10494  rexanuz2  11556  even2n  12440  infpn2  13082  xpsfrnel2  13434  issubg  13765  isnsg  13794  issrg  13984  iscrng2  14034  isrim0  14181  issubrng  14219  issubrg  14241  rrgval  14282  islssm  14377  islidlm  14499  2idlval  14522  2idlelb  14525  istopon  14743  ishmeo  15034  ismet2  15084  edgval  15917  istrl  16242  isclwwlk  16251  clwwlkn0  16265  isclwwlkn  16270  clwwlknonmpo  16285  clwwlknon  16286  clwwlk0on0  16288  iseupth  16304