Theorem pm5.21nii 712

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  1445  elrabf  2974  sbcco  3067  sbc5  3069  sbcan  3088  sbcor  3090  sbcal  3097  sbcex2  3099  sbcel1v  3108  eldif  3223  elun  3364  elin  3406  elif  3638  rabsnif  3763  eluni  3922  eliun  4000  elopab  4381  opelopabsb  4383  opeliunxp  4810  opeliunxp2  4900  elxp4  5255  elxp5  5256  fsn2  5856  isocnv2  5991  elxp6  6376  elxp7  6377  opeliunxp2f  6482  brtpos2  6495  tpostpos  6508  ecdmn0m  6824  elixpsn  6983  bren  6996  omniwomnimkv  7471  elinp  7805  recexprlemell  7953  recexprlemelu  7954  gt0srpr  8079  ltresr  8170  eluz2  9877  elfz2  10368  infssuzex  10615  rexanuz2  11701  even2n  12585  infpn2  13291  xpsfrnel2  13610  issubg  13926  isnsg  13955  issrg  14208  iscrng2  14258  opprringb  14324  isrim0  14406  opprlring  14442  issubrng  14445  issubrg  14467  rrgval  14508  opprdrng  14558  islssm  14631  islidlm  14753  2idlval  14776  2idlelb  14779  istopon  15004  ishmeo  15295  ismet2  15345  edgval  16181  istrl  16506  isclwwlk  16515  clwwlkn0  16529  isclwwlkn  16534  clwwlknonmpo  16549  clwwlknon  16550  clwwlk0on0  16552  iseupth  16568