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  2958  sbcco  3051  sbc5  3053  sbcan  3072  sbcor  3074  sbcal  3081  sbcex2  3083  sbcel1v  3092  eldif  3207  elun  3346  elin  3388  elif  3615  rabsnif  3736  eluni  3894  eliun  3972  elopab  4350  opelopabsb  4352  opeliunxp  4779  opeliunxp2  4868  elxp4  5222  elxp5  5223  fsn2  5817  isocnv2  5948  elxp6  6327  elxp7  6328  opeliunxp2f  6399  brtpos2  6412  tpostpos  6425  ecdmn0m  6741  elixpsn  6899  bren  6912  omniwomnimkv  7360  elinp  7687  recexprlemell  7835  recexprlemelu  7836  gt0srpr  7961  ltresr  8052  eluz2  9754  elfz2  10243  infssuzex  10486  rexanuz2  11545  even2n  12428  infpn2  13070  xpsfrnel2  13422  issubg  13753  isnsg  13782  issrg  13971  iscrng2  14021  isrim0  14168  issubrng  14206  issubrg  14228  rrgval  14269  islssm  14364  islidlm  14486  2idlval  14509  2idlelb  14512  istopon  14730  ishmeo  15021  ismet2  15071  edgval  15904  istrl  16194  isclwwlk  16203  clwwlkn0  16217  isclwwlkn  16222  clwwlknonmpo  16237  clwwlknon  16238  clwwlk0on0  16240  iseupth  16256