Theorem pm5.21nii 712

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  1445  elrabf  2961  sbcco  3054  sbc5  3056  sbcan  3075  sbcor  3077  sbcal  3084  sbcex2  3086  sbcel1v  3095  eldif  3210  elun  3350  elin  3392  elif  3621  rabsnif  3742  eluni  3901  eliun  3979  elopab  4358  opelopabsb  4360  opeliunxp  4787  opeliunxp2  4876  elxp4  5231  elxp5  5232  fsn2  5829  isocnv2  5963  elxp6  6341  elxp7  6342  opeliunxp2f  6447  brtpos2  6460  tpostpos  6473  ecdmn0m  6789  elixpsn  6947  bren  6960  omniwomnimkv  7409  elinp  7737  recexprlemell  7885  recexprlemelu  7886  gt0srpr  8011  ltresr  8102  eluz2  9804  elfz2  10293  infssuzex  10537  rexanuz2  11612  even2n  12496  infpn2  13138  xpsfrnel2  13490  issubg  13821  isnsg  13850  issrg  14040  iscrng2  14090  isrim0  14237  issubrng  14275  issubrg  14297  rrgval  14338  islssm  14433  islidlm  14555  2idlval  14578  2idlelb  14581  istopon  14804  ishmeo  15095  ismet2  15145  edgval  15981  istrl  16306  isclwwlk  16315  clwwlkn0  16329  isclwwlkn  16334  clwwlknonmpo  16349  clwwlknon  16350  clwwlk0on0  16352  iseupth  16368