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  2914  sbcco  3007  sbc5  3009  sbcan  3028  sbcor  3030  sbcal  3037  sbcex2  3039  sbcel1v  3048  eldif  3162  elun  3300  elin  3342  eluni  3838  eliun  3916  elopab  4288  opelopabsb  4290  opeliunxp  4714  opeliunxp2  4802  elxp4  5153  elxp5  5154  fsn2  5732  isocnv2  5855  elxp6  6222  elxp7  6223  opeliunxp2f  6291  brtpos2  6304  tpostpos  6317  ecdmn0m  6631  elixpsn  6789  bren  6801  omniwomnimkv  7226  elinp  7534  recexprlemell  7682  recexprlemelu  7683  gt0srpr  7808  ltresr  7899  eluz2  9598  elfz2  10081  rexanuz2  11135  even2n  12015  infssuzex  12086  infpn2  12613  xpsfrnel2  12929  issubg  13243  isnsg  13272  issrg  13461  iscrng2  13511  isrim0  13657  issubrng  13695  issubrg  13717  rrgval  13758  islssm  13853  islidlm  13975  2idlval  13998  2idlelb  14001  istopon  14181  ishmeo  14472  ismet2  14522