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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3652  rabsnif  3778  eluni  3938  eliun  4016  elopab  4402  opelopabsb  4404  opeliunxp  4832  opeliunxp2  4922  elxp4  5278  elxp5  5279  fsn2  5885  isocnv2  6021  elxp6  6407  elxp7  6408  opeliunxp2f  6513  brtpos2  6526  tpostpos  6539  ecdmn0m  6855  elixpsn  7021  bren  7034  omniwomnimkv  7513  elinp  7847  recexprlemell  7995  recexprlemelu  7996  gt0srpr  8121  ltresr  8212  eluz2  9943  elfz2  10435  infssuzex  10683  rexanuz2  11779  even2n  12666  infpn2  13405  xpsfrnel2  13726  issubg  14035  isnsg  14064  cntrval  14151  mgpplusg  14329  mgpbas  14332  ringidval  14372  issrg  14376  iscrng2  14426  opprringb  14495  isrim0  14577  opprlring  14613  issubrng  14616  issubrg  14638  rrgval  14679  opprdrng  14729  islssm  14803  islidlm  14925  2idlval  14948  2idlelb  14951  asclfval  15130  istopon  15239  ishmeo  15530  ismet2  15580  edgval  16506  istrl  16831  isclwwlk  16840  clwwlkn0  16854  isclwwlkn  16859  clwwlknonmpo  16874  clwwlknon  16875  clwwlk0on0  16877  iseupth  16893