Theorem pm5.21nii 706

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  1420  elrabf  2934  sbcco  3027  sbc5  3029  sbcan  3048  sbcor  3050  sbcal  3057  sbcex2  3059  sbcel1v  3068  eldif  3183  elun  3322  elin  3364  elif  3591  eluni  3867  eliun  3945  elopab  4322  opelopabsb  4324  opeliunxp  4748  opeliunxp2  4836  elxp4  5189  elxp5  5190  fsn2  5777  isocnv2  5904  elxp6  6278  elxp7  6279  opeliunxp2f  6347  brtpos2  6360  tpostpos  6373  ecdmn0m  6687  elixpsn  6845  bren  6858  omniwomnimkv  7295  elinp  7622  recexprlemell  7770  recexprlemelu  7771  gt0srpr  7896  ltresr  7987  eluz2  9689  elfz2  10172  infssuzex  10413  rexanuz2  11417  even2n  12300  infpn2  12942  xpsfrnel2  13293  issubg  13624  isnsg  13653  issrg  13842  iscrng2  13892  isrim0  14038  issubrng  14076  issubrg  14098  rrgval  14139  islssm  14234  islidlm  14356  2idlval  14379  2idlelb  14382  istopon  14600  ishmeo  14891  ismet2  14941