Theorem pm5.21nii 716

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  1449  elrabf  2980  sbcco  3073  sbc5  3075  sbcan  3094  sbcor  3096  sbcal  3103  sbcex2  3105  sbcel1v  3114  eldif  3229  elun  3370  elin  3412  elif  3649  rabsnif  3774  eluni  3933  eliun  4011  elopab  4395  opelopabsb  4397  opeliunxp  4825  opeliunxp2  4915  elxp4  5270  elxp5  5271  fsn2  5873  isocnv2  6008  elxp6  6393  elxp7  6394  opeliunxp2f  6499  brtpos2  6512  tpostpos  6525  ecdmn0m  6841  elixpsn  7007  bren  7020  omniwomnimkv  7497  elinp  7831  recexprlemell  7979  recexprlemelu  7980  gt0srpr  8105  ltresr  8196  eluz2  9906  elfz2  10397  infssuzex  10644  rexanuz2  11735  even2n  12619  infpn2  13325  xpsfrnel2  13644  issubg  13953  isnsg  13982  issrg  14243  iscrng2  14293  opprringb  14359  isrim0  14441  opprlring  14477  issubrng  14480  issubrg  14502  rrgval  14543  opprdrng  14593  islssm  14666  islidlm  14788  2idlval  14811  2idlelb  14814  istopon  15037  ishmeo  15328  ismet2  15378  edgval  16215  istrl  16540  isclwwlk  16549  clwwlkn0  16563  isclwwlkn  16568  clwwlknonmpo  16583  clwwlknon  16584  clwwlk0on0  16586  iseupth  16602