Theorem pm5.21nii 709

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  1442  elrabf  2958  sbcco  3051  sbc5  3053  sbcan  3072  sbcor  3074  sbcal  3081  sbcex2  3083  sbcel1v  3092  eldif  3207  elun  3346  elin  3388  elif  3615  rabsnif  3736  eluni  3894  eliun  3972  elopab  4350  opelopabsb  4352  opeliunxp  4779  opeliunxp2  4868  elxp4  5222  elxp5  5223  fsn2  5817  isocnv2  5948  elxp6  6327  elxp7  6328  opeliunxp2f  6399  brtpos2  6412  tpostpos  6425  ecdmn0m  6741  elixpsn  6899  bren  6912  omniwomnimkv  7357  elinp  7684  recexprlemell  7832  recexprlemelu  7833  gt0srpr  7958  ltresr  8049  eluz2  9751  elfz2  10240  infssuzex  10483  rexanuz2  11542  even2n  12425  infpn2  13067  xpsfrnel2  13419  issubg  13750  isnsg  13779  issrg  13968  iscrng2  14018  isrim0  14165  issubrng  14203  issubrg  14225  rrgval  14266  islssm  14361  islidlm  14483  2idlval  14506  2idlelb  14509  istopon  14727  ishmeo  15018  ismet2  15068  edgval  15901  istrl  16180  isclwwlk  16189  clwwlkn0  16203  isclwwlkn  16208  clwwlknonmpo  16223  clwwlknon  16224  clwwlk0on0  16226  iseupth  16242