Theorem pm5.21nii 709

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  1442  elrabf  2957  sbcco  3050  sbc5  3052  sbcan  3071  sbcor  3073  sbcal  3080  sbcex2  3082  sbcel1v  3091  eldif  3206  elun  3345  elin  3387  elif  3614  eluni  3890  eliun  3968  elopab  4345  opelopabsb  4347  opeliunxp  4773  opeliunxp2  4861  elxp4  5215  elxp5  5216  fsn2  5808  isocnv2  5935  elxp6  6313  elxp7  6314  opeliunxp2f  6382  brtpos2  6395  tpostpos  6408  ecdmn0m  6722  elixpsn  6880  bren  6893  omniwomnimkv  7330  elinp  7657  recexprlemell  7805  recexprlemelu  7806  gt0srpr  7931  ltresr  8022  eluz2  9724  elfz2  10207  infssuzex  10448  rexanuz2  11497  even2n  12380  infpn2  13022  xpsfrnel2  13374  issubg  13705  isnsg  13734  issrg  13923  iscrng2  13973  isrim0  14119  issubrng  14157  issubrg  14179  rrgval  14220  islssm  14315  islidlm  14437  2idlval  14460  2idlelb  14463  istopon  14681  ishmeo  14972  ismet2  15022