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  1410  elrabf  2903  sbcco  2996  sbc5  2998  sbcan  3017  sbcor  3019  sbcal  3026  sbcex2  3028  sbcel1v  3037  eldif  3150  elun  3288  elin  3330  eluni  3824  eliun  3902  elopab  4270  opelopabsb  4272  opeliunxp  4693  opeliunxp2  4779  elxp4  5128  elxp5  5129  fsn2  5703  isocnv2  5826  elxp6  6183  elxp7  6184  opeliunxp2f  6252  brtpos2  6265  tpostpos  6278  ecdmn0m  6590  elixpsn  6748  bren  6760  omniwomnimkv  7178  elinp  7486  recexprlemell  7634  recexprlemelu  7635  gt0srpr  7760  ltresr  7851  eluz2  9547  elfz2  10028  rexanuz2  11013  even2n  11892  infssuzex  11963  infpn2  12470  xpsfrnel2  12783  issubg  13064  isnsg  13093  issrg  13212  iscrng2  13262  issubrng  13414  issubrg  13436  islssm  13541  islidlm  13663  2idlelb  13684  istopon  13784  ishmeo  14075  ismet2  14125