Theorem pm5.21nii 653

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 174	. 2 |- ( ph -> ch )
5		pm5.21ni.2	. . . 4 |- ( ch -> ps )
6	5, 2	syl 14	. . 3 |- ( ch -> ( ph <-> ch ) )
7	6	ibir 175	. 2 |- ( ch -> ph )
8	4, 7	impbii 124	1 |- ( ph <-> ch )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anxordi  1332  elrabf  2748  sbcco  2837  sbc5  2839  sbcan  2857  sbcor  2859  sbcal  2866  sbcex2  2868  sbcel1v  2877  eldif  2983  elun  3114  elin  3156  eluni  3612  eliun  3690  elopab  4021  opelopabsb  4023  opeliunxp  4421  opeliunxp2  4504  elxp4  4838  elxp5  4839  fsn2  5369  isocnv2  5483  elxp6  5827  elxp7  5828  brtpos2  5900  tpostpos  5913  ecdmn0m  6214  bren  6294  elinp  6726  recexprlemell  6874  recexprlemelu  6875  gt0srpr  6987  ltresr  7069  eluz2  8706  elfz2  9112  rexanuz2  10015  even2n  10418  infssuzex  10489