Theorem pm5.21nii 699

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	|- ( ph -> ps )
pm5.21ni.2	|- ( ch -> ps )
pm5.21nii.3	|- ( ps -> ( ph <-> ch ) )

Assertion

Ref	Expression
pm5.21nii	|- ( ph <-> ch )

Proof of Theorem pm5.21nii

Step	Hyp	Ref	Expression
1		pm5.21ni.1	. . . 4 |- ( ph -> ps )
2		pm5.21nii.3	. . . 4 |- ( ps -> ( ph <-> ch ) )
3	1, 2	syl 14	. . 3 |- ( ph -> ( ph <-> ch ) )
4	3	ibi 175	. 2 |- ( ph -> ch )
5		pm5.21ni.2	. . . 4 |- ( ch -> ps )
6	5, 2	syl 14	. . 3 |- ( ch -> ( ph <-> ch ) )
7	6	ibir 176	. 2 |- ( ch -> ph )
8	4, 7	impbii 125	1 |- ( ph <-> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anxordi  1395  elrabf  2884  sbcco  2976  sbc5  2978  sbcan  2997  sbcor  2999  sbcal  3006  sbcex2  3008  sbcel1v  3017  eldif  3130  elun  3268  elin  3310  eluni  3797  eliun  3875  elopab  4241  opelopabsb  4243  opeliunxp  4664  opeliunxp2  4749  elxp4  5096  elxp5  5097  fsn2  5667  isocnv2  5788  elxp6  6145  elxp7  6146  opeliunxp2f  6214  brtpos2  6227  tpostpos  6240  ecdmn0m  6551  elixpsn  6709  bren  6721  omniwomnimkv  7139  elinp  7423  recexprlemell  7571  recexprlemelu  7572  gt0srpr  7697  ltresr  7788  eluz2  9480  elfz2  9959  rexanuz2  10942  even2n  11820  infssuzex  11891  infpn2  12398  istopon  12726  ishmeo  13019  ismet2  13069