Theorem pm5.21nii 705

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  1411  elrabf  2918  sbcco  3011  sbc5  3013  sbcan  3032  sbcor  3034  sbcal  3041  sbcex2  3043  sbcel1v  3052  eldif  3166  elun  3305  elin  3347  eluni  3843  eliun  3921  elopab  4293  opelopabsb  4295  opeliunxp  4719  opeliunxp2  4807  elxp4  5158  elxp5  5159  fsn2  5739  isocnv2  5862  elxp6  6236  elxp7  6237  opeliunxp2f  6305  brtpos2  6318  tpostpos  6331  ecdmn0m  6645  elixpsn  6803  bren  6815  omniwomnimkv  7242  elinp  7560  recexprlemell  7708  recexprlemelu  7709  gt0srpr  7834  ltresr  7925  eluz2  9626  elfz2  10109  infssuzex  10342  rexanuz2  11175  even2n  12058  infpn2  12700  xpsfrnel2  13050  issubg  13381  isnsg  13410  issrg  13599  iscrng2  13649  isrim0  13795  issubrng  13833  issubrg  13855  rrgval  13896  islssm  13991  islidlm  14113  2idlval  14136  2idlelb  14139  istopon  14357  ishmeo  14648  ismet2  14698