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  2927  sbcco  3020  sbc5  3022  sbcan  3041  sbcor  3043  sbcal  3050  sbcex2  3052  sbcel1v  3061  eldif  3175  elun  3314  elin  3356  eluni  3853  eliun  3931  elopab  4304  opelopabsb  4306  opeliunxp  4730  opeliunxp2  4818  elxp4  5170  elxp5  5171  fsn2  5754  isocnv2  5881  elxp6  6255  elxp7  6256  opeliunxp2f  6324  brtpos2  6337  tpostpos  6350  ecdmn0m  6664  elixpsn  6822  bren  6835  omniwomnimkv  7269  elinp  7587  recexprlemell  7735  recexprlemelu  7736  gt0srpr  7861  ltresr  7952  eluz2  9654  elfz2  10137  infssuzex  10376  rexanuz2  11302  even2n  12185  infpn2  12827  xpsfrnel2  13178  issubg  13509  isnsg  13538  issrg  13727  iscrng2  13777  isrim0  13923  issubrng  13961  issubrg  13983  rrgval  14024  islssm  14119  islidlm  14241  2idlval  14264  2idlelb  14267  istopon  14485  ishmeo  14776  ismet2  14826