Theorem pm5.21nii 716

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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anxordi  1449  elrabf  2980  sbcco  3073  sbc5  3075  sbcan  3094  sbcor  3096  sbcal  3103  sbcex2  3105  sbcel1v  3114  eldif  3229  elun  3370  elin  3412  elif  3652  rabsnif  3778  eluni  3938  eliun  4016  elopab  4400  opelopabsb  4402  opeliunxp  4830  opeliunxp2  4920  elxp4  5275  elxp5  5276  fsn2  5882  isocnv2  6018  elxp6  6403  elxp7  6404  opeliunxp2f  6509  brtpos2  6522  tpostpos  6535  ecdmn0m  6851  elixpsn  7017  bren  7030  omniwomnimkv  7508  elinp  7842  recexprlemell  7990  recexprlemelu  7991  gt0srpr  8116  ltresr  8207  eluz2  9937  elfz2  10429  infssuzex  10677  rexanuz2  11773  even2n  12660  infpn2  13399  xpsfrnel2  13720  issubg  14029  isnsg  14058  cntrval  14145  mgpplusg  14313  mgpbas  14316  ringidval  14356  issrg  14360  iscrng2  14410  opprringb  14477  isrim0  14559  opprlring  14595  issubrng  14598  issubrg  14620  rrgval  14661  opprdrng  14711  islssm  14785  islidlm  14907  2idlval  14930  2idlelb  14933  asclfval  15112  istopon  15213  ishmeo  15504  ismet2  15554  edgval  16480  istrl  16805  isclwwlk  16814  clwwlkn0  16828  isclwwlkn  16833  clwwlknonmpo  16848  clwwlknon  16849  clwwlk0on0  16851  iseupth  16867