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  2961  sbcco  3054  sbc5  3056  sbcan  3075  sbcor  3077  sbcal  3084  sbcex2  3086  sbcel1v  3095  eldif  3210  elun  3350  elin  3392  elif  3621  rabsnif  3742  eluni  3901  eliun  3979  elopab  4358  opelopabsb  4360  opeliunxp  4787  opeliunxp2  4876  elxp4  5231  elxp5  5232  fsn2  5829  isocnv2  5963  elxp6  6341  elxp7  6342  opeliunxp2f  6447  brtpos2  6460  tpostpos  6473  ecdmn0m  6789  elixpsn  6947  bren  6960  omniwomnimkv  7409  elinp  7737  recexprlemell  7885  recexprlemelu  7886  gt0srpr  8011  ltresr  8102  eluz2  9805  elfz2  10295  infssuzex  10539  rexanuz2  11614  even2n  12498  infpn2  13140  xpsfrnel2  13492  issubg  13823  isnsg  13852  issrg  14042  iscrng2  14092  isrim0  14239  issubrng  14277  issubrg  14299  rrgval  14340  islssm  14436  islidlm  14558  2idlval  14581  2idlelb  14584  istopon  14807  ishmeo  15098  ismet2  15148  edgval  15984  istrl  16309  isclwwlk  16318  clwwlkn0  16332  isclwwlkn  16337  clwwlknonmpo  16352  clwwlknon  16353  clwwlk0on0  16355  iseupth  16371