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  2918  sbcco  3011  sbc5  3013  sbcan  3032  sbcor  3034  sbcal  3041  sbcex2  3043  sbcel1v  3052  eldif  3166  elun  3304  elin  3346  eluni  3842  eliun  3920  elopab  4292  opelopabsb  4294  opeliunxp  4718  opeliunxp2  4806  elxp4  5157  elxp5  5158  fsn2  5736  isocnv2  5859  elxp6  6227  elxp7  6228  opeliunxp2f  6296  brtpos2  6309  tpostpos  6322  ecdmn0m  6636  elixpsn  6794  bren  6806  omniwomnimkv  7233  elinp  7541  recexprlemell  7689  recexprlemelu  7690  gt0srpr  7815  ltresr  7906  eluz2  9607  elfz2  10090  infssuzex  10323  rexanuz2  11156  even2n  12039  infpn2  12673  xpsfrnel2  12989  issubg  13303  isnsg  13332  issrg  13521  iscrng2  13571  isrim0  13717  issubrng  13755  issubrg  13777  rrgval  13818  islssm  13913  islidlm  14035  2idlval  14058  2idlelb  14061  istopon  14249  ishmeo  14540  ismet2  14590