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  9877  elfz2  10368  infssuzex  10615  rexanuz2  11701  even2n  12585  infpn2  13291  xpsfrnel2  13643  issubg  13974  isnsg  14003  issrg  14193  iscrng2  14243  opprringb  14309  isrim0  14391  opprlring  14427  issubrng  14430  issubrg  14452  rrgval  14493  opprdrng  14543  islssm  14617  islidlm  14739  2idlval  14762  2idlelb  14765  istopon  14990  ishmeo  15281  ismet2  15331  edgval  16167  istrl  16492  isclwwlk  16501  clwwlkn0  16515  isclwwlkn  16520  clwwlknonmpo  16535  clwwlknon  16536  clwwlk0on0  16538  iseupth  16554