Theorem pm5.21nii 712

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  1445  elrabf  2971  sbcco  3064  sbc5  3066  sbcan  3085  sbcor  3087  sbcal  3094  sbcex2  3096  sbcel1v  3105  eldif  3220  elun  3360  elin  3402  elif  3634  rabsnif  3758  eluni  3917  eliun  3995  elopab  4376  opelopabsb  4378  opeliunxp  4805  opeliunxp2  4895  elxp4  5250  elxp5  5251  fsn2  5851  isocnv2  5985  elxp6  6363  elxp7  6364  opeliunxp2f  6469  brtpos2  6482  tpostpos  6495  ecdmn0m  6811  elixpsn  6970  bren  6983  omniwomnimkv  7458  elinp  7789  recexprlemell  7937  recexprlemelu  7938  gt0srpr  8063  ltresr  8154  eluz2  9859  elfz2  10349  infssuzex  10593  rexanuz2  11676  even2n  12560  infpn2  13207  xpsfrnel2  13559  issubg  13890  isnsg  13919  issrg  14109  iscrng2  14159  isrim0  14306  issubrng  14344  issubrg  14366  rrgval  14407  islssm  14505  islidlm  14627  2idlval  14650  2idlelb  14653  istopon  14878  ishmeo  15169  ismet2  15219  edgval  16055  istrl  16380  isclwwlk  16389  clwwlkn0  16403  isclwwlkn  16408  clwwlknonmpo  16423  clwwlknon  16424  clwwlk0on0  16426  iseupth  16442