Theorem pm5.21nii 704

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 176	. 2 |- ( ph -> ch )
5		pm5.21ni.2	. . . 4 |- ( ch -> ps )
6	5, 2	syl 14	. . 3 |- ( ch -> ( ph <-> ch ) )
7	6	ibir 177	. 2 |- ( ch -> ph )
8	4, 7	impbii 126	1 |- ( ph <-> ch )

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  1400  elrabf  2891  sbcco  2984  sbc5  2986  sbcan  3005  sbcor  3007  sbcal  3014  sbcex2  3016  sbcel1v  3025  eldif  3138  elun  3276  elin  3318  eluni  3812  eliun  3890  elopab  4258  opelopabsb  4260  opeliunxp  4681  opeliunxp2  4767  elxp4  5116  elxp5  5117  fsn2  5690  isocnv2  5812  elxp6  6169  elxp7  6170  opeliunxp2f  6238  brtpos2  6251  tpostpos  6264  ecdmn0m  6576  elixpsn  6734  bren  6746  omniwomnimkv  7164  elinp  7472  recexprlemell  7620  recexprlemelu  7621  gt0srpr  7746  ltresr  7837  eluz2  9533  elfz2  10014  rexanuz2  10999  even2n  11878  infssuzex  11949  infpn2  12456  xpsfrnel2  12764  issubg  13031  isnsg  13060  issrg  13146  iscrng2  13196  issubrg  13340  istopon  13483  ishmeo  13774  ismet2  13824