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  3891  eliun  3969  elopab  4346  opelopabsb  4348  opeliunxp  4774  opeliunxp2  4862  elxp4  5216  elxp5  5217  fsn2  5809  isocnv2  5936  elxp6  6315  elxp7  6316  opeliunxp2f  6384  brtpos2  6397  tpostpos  6410  ecdmn0m  6724  elixpsn  6882  bren  6895  omniwomnimkv  7334  elinp  7661  recexprlemell  7809  recexprlemelu  7810  gt0srpr  7935  ltresr  8026  eluz2  9728  elfz2  10211  infssuzex  10453  rexanuz2  11502  even2n  12385  infpn2  13027  xpsfrnel2  13379  issubg  13710  isnsg  13739  issrg  13928  iscrng2  13978  isrim0  14125  issubrng  14163  issubrg  14185  rrgval  14226  islssm  14321  islidlm  14443  2idlval  14466  2idlelb  14469  istopon  14687  ishmeo  14978  ismet2  15028