Theorem pm5.21nii 604

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  1272  elrabf  2667  sbcco  2756  sbc5  2758  sbcan  2776  sbcor  2778  sbcal  2781  sbcex2  2783  eldif  2898  elun  3055  elin  3097  eluni  3549  eliun  3627  elopab  3961  opelopabsb  3963  opeliunxp  4313  opeliunxp2  4394  elxp4  4726  elxp5  4727  fsn2  5253  isocnv2  5368  elxp6  5710  elxp7  5711  brtpos2  5779  tpostpos  5792  ecdmn0m  6050  elinp  6317  recexprlemell  6446  recexprlemelu  6447  gt0srpr  6489  ltresr  6548  eluz2  8047