Theorem pm5.21nii 711

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  1444  elrabf  2960  sbcco  3053  sbc5  3055  sbcan  3074  sbcor  3076  sbcal  3083  sbcex2  3085  sbcel1v  3094  eldif  3209  elun  3348  elin  3390  elif  3617  rabsnif  3738  eluni  3896  eliun  3974  elopab  4352  opelopabsb  4354  opeliunxp  4781  opeliunxp2  4870  elxp4  5224  elxp5  5225  fsn2  5821  isocnv2  5952  elxp6  6331  elxp7  6332  opeliunxp2f  6403  brtpos2  6416  tpostpos  6429  ecdmn0m  6745  elixpsn  6903  bren  6916  omniwomnimkv  7365  elinp  7693  recexprlemell  7841  recexprlemelu  7842  gt0srpr  7967  ltresr  8058  eluz2  9760  elfz2  10249  infssuzex  10492  rexanuz2  11551  even2n  12434  infpn2  13076  xpsfrnel2  13428  issubg  13759  isnsg  13788  issrg  13977  iscrng2  14027  isrim0  14174  issubrng  14212  issubrg  14234  rrgval  14275  islssm  14370  islidlm  14492  2idlval  14515  2idlelb  14518  istopon  14736  ishmeo  15027  ismet2  15077  edgval  15910  istrl  16235  isclwwlk  16244  clwwlkn0  16258  isclwwlkn  16263  clwwlknonmpo  16278  clwwlknon  16279  clwwlk0on0  16281  iseupth  16297