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  1419  elrabf  2926  sbcco  3019  sbc5  3021  sbcan  3040  sbcor  3042  sbcal  3049  sbcex2  3051  sbcel1v  3060  eldif  3174  elun  3313  elin  3355  eluni  3852  eliun  3930  elopab  4303  opelopabsb  4305  opeliunxp  4729  opeliunxp2  4817  elxp4  5169  elxp5  5170  fsn2  5753  isocnv2  5880  elxp6  6254  elxp7  6255  opeliunxp2f  6323  brtpos2  6336  tpostpos  6349  ecdmn0m  6663  elixpsn  6821  bren  6834  omniwomnimkv  7268  elinp  7586  recexprlemell  7734  recexprlemelu  7735  gt0srpr  7860  ltresr  7951  eluz2  9653  elfz2  10136  infssuzex  10374  rexanuz2  11273  even2n  12156  infpn2  12798  xpsfrnel2  13149  issubg  13480  isnsg  13509  issrg  13698  iscrng2  13748  isrim0  13894  issubrng  13932  issubrg  13954  rrgval  13995  islssm  14090  islidlm  14212  2idlval  14235  2idlelb  14238  istopon  14456  ishmeo  14747  ismet2  14797