Theorem pm5.21nii 716

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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anxordi  1449  elrabf  2980  sbcco  3073  sbc5  3075  sbcan  3094  sbcor  3096  sbcal  3103  sbcex2  3105  sbcel1v  3114  eldif  3229  elun  3370  elin  3412  elif  3652  rabsnif  3778  eluni  3938  eliun  4016  elopab  4402  opelopabsb  4404  opeliunxp  4832  opeliunxp2  4922  elxp4  5278  elxp5  5279  fsn2  5885  isocnv2  6021  elxp6  6407  elxp7  6408  opeliunxp2f  6514  brtpos2  6527  tpostpos  6540  ecdmn0m  6856  elixpsn  7023  bren  7036  omniwomnimkv  7513  elinp  7847  recexprlemell  7995  recexprlemelu  7996  gt0srpr  8121  ltresr  8212  eluz2  9942  elfz2  10434  infssuzex  10682  rexanuz2  11778  even2n  12665  infpn2  13404  xpsfrnel2  13725  issubg  14034  isnsg  14063  cntrval  14150  mgpplusg  14328  mgpbas  14331  ringidval  14371  issrg  14375  iscrng2  14425  opprringb  14494  isrim0  14576  opprlring  14612  issubrng  14615  issubrg  14637  rrgval  14678  opprdrng  14728  islssm  14802  islidlm  14924  2idlval  14947  2idlelb  14950  asclfval  15129  mplbas  15223  istopon  15256  ishmeo  15547  ismet2  15597  edgval  16523  istrl  16848  isclwwlk  16857  clwwlkn0  16871  isclwwlkn  16876  clwwlknonmpo  16891  clwwlknon  16892  clwwlk0on0  16894  iseupth  16910