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  2974  sbcco  3067  sbc5  3069  sbcan  3088  sbcor  3090  sbcal  3097  sbcex2  3099  sbcel1v  3108  eldif  3223  elun  3364  elin  3406  elif  3638  rabsnif  3763  eluni  3922  eliun  4000  elopab  4381  opelopabsb  4383  opeliunxp  4810  opeliunxp2  4900  elxp4  5255  elxp5  5256  fsn2  5856  isocnv2  5991  elxp6  6376  elxp7  6377  opeliunxp2f  6482  brtpos2  6495  tpostpos  6508  ecdmn0m  6824  elixpsn  6983  bren  6996  omniwomnimkv  7471  elinp  7805  recexprlemell  7953  recexprlemelu  7954  gt0srpr  8079  ltresr  8170  eluz2  9880  elfz2  10371  infssuzex  10618  rexanuz2  11705  even2n  12589  infpn2  13295  xpsfrnel2  13614  issubg  13930  isnsg  13959  issrg  14212  iscrng2  14262  opprringb  14328  isrim0  14410  opprlring  14446  issubrng  14449  issubrg  14471  rrgval  14512  opprdrng  14562  islssm  14635  islidlm  14757  2idlval  14780  2idlelb  14783  istopon  15008  ishmeo  15299  ismet2  15349  edgval  16185  istrl  16510  isclwwlk  16519  clwwlkn0  16533  isclwwlkn  16538  clwwlknonmpo  16553  clwwlknon  16554  clwwlk0on0  16556  iseupth  16572