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  2915  sbcco  3008  sbc5  3010  sbcan  3029  sbcor  3031  sbcal  3038  sbcex2  3040  sbcel1v  3049  eldif  3163  elun  3301  elin  3343  eluni  3839  eliun  3917  elopab  4289  opelopabsb  4291  opeliunxp  4715  opeliunxp2  4803  elxp4  5154  elxp5  5155  fsn2  5733  isocnv2  5856  elxp6  6224  elxp7  6225  opeliunxp2f  6293  brtpos2  6306  tpostpos  6319  ecdmn0m  6633  elixpsn  6791  bren  6803  omniwomnimkv  7228  elinp  7536  recexprlemell  7684  recexprlemelu  7685  gt0srpr  7810  ltresr  7901  eluz2  9601  elfz2  10084  rexanuz2  11138  even2n  12018  infssuzex  12089  infpn2  12616  xpsfrnel2  12932  issubg  13246  isnsg  13275  issrg  13464  iscrng2  13514  isrim0  13660  issubrng  13698  issubrg  13720  rrgval  13761  islssm  13856  islidlm  13978  2idlval  14001  2idlelb  14004  istopon  14192  ishmeo  14483  ismet2  14533