Theorem pm5.21nii 705

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  1411  elrabf  2918  sbcco  3011  sbc5  3013  sbcan  3032  sbcor  3034  sbcal  3041  sbcex2  3043  sbcel1v  3052  eldif  3166  elun  3305  elin  3347  eluni  3843  eliun  3921  elopab  4293  opelopabsb  4295  opeliunxp  4719  opeliunxp2  4807  elxp4  5158  elxp5  5159  fsn2  5739  isocnv2  5862  elxp6  6236  elxp7  6237  opeliunxp2f  6305  brtpos2  6318  tpostpos  6331  ecdmn0m  6645  elixpsn  6803  bren  6815  omniwomnimkv  7242  elinp  7558  recexprlemell  7706  recexprlemelu  7707  gt0srpr  7832  ltresr  7923  eluz2  9624  elfz2  10107  infssuzex  10340  rexanuz2  11173  even2n  12056  infpn2  12698  xpsfrnel2  13048  issubg  13379  isnsg  13408  issrg  13597  iscrng2  13647  isrim0  13793  issubrng  13831  issubrg  13853  rrgval  13894  islssm  13989  islidlm  14111  2idlval  14134  2idlelb  14137  istopon  14333  ishmeo  14624  ismet2  14674