Theorem pm5.21nii 607

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anxordi  1274  elrabf  2673  sbcco  2762  sbc5  2764  sbcan  2782  sbcor  2784  sbcal  2787  sbcex2  2789  eldif  2904  elun  3061  elin  3103  eluni  3557  eliun  3635  elopab  3969  opelopabsb  3971  opeliunxp  4322  opeliunxp2  4403  elxp4  4735  elxp5  4736  fsn2  5262  isocnv2  5377  elxp6  5719  elxp7  5720  brtpos2  5788  tpostpos  5801  ecdmn0m  6059  elinp  6328  recexprlemell  6456  recexprlemelu  6457  gt0srpr  6495  ltresr  6550