Theorem pm5.21nii 661

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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anxordi  1346  elrabf  2791  sbcco  2883  sbc5  2885  sbcan  2903  sbcor  2905  sbcal  2912  sbcex2  2914  sbcel1v  2923  eldif  3030  elun  3164  elin  3206  eluni  3686  eliun  3764  elopab  4118  opelopabsb  4120  opeliunxp  4532  opeliunxp2  4617  elxp4  4962  elxp5  4963  fsn2  5526  isocnv2  5645  elxp6  5998  elxp7  5999  opeliunxp2f  6065  brtpos2  6078  tpostpos  6091  ecdmn0m  6401  elixpsn  6559  bren  6571  elinp  7183  recexprlemell  7331  recexprlemelu  7332  gt0srpr  7444  ltresr  7526  eluz2  9182  elfz2  9638  rexanuz2  10603  even2n  11366  infssuzex  11437  istopon  11962  ismet2  12282