Theorem pm5.21nii 342

Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.)

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.21nii.3	. 2 |- (ps -> (ph <-> ch))
2		pm5.21ni.1	. . 3 |- (ph -> ps)
3		pm5.21ni.2	. . 3 |- (ch -> ps)
4	2, 3	pm5.21ni 341	. 2 |- (-. ps -> (ph <-> ch))
5	1, 4	pm2.61i 156	1 |- (ph <-> ch)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  elrabf  2993  sbcco  3068  sbc5  3070  sbcan  3088  sbcor  3090  sbcal  3093  sbcex2  3095  elin  3219  elun  3220  eluni  3894  eliun  3973  el1c  4139  elxpk  4196  eladdc  4398  elopab  4696  opelopabsb  4697  elima  4754  brsi  4761  epelc  4765  opeliunxp  4820  opeliunxp2  4822  br1st  4858  br2nd  4859  brswap2  4860  brco  4883  brcnv  4892  elimasn  5019  opbr1st  5501  opbr2nd  5502  brswap  5509  trtxp  5781  elfix  5787  otelins2  5791  otelins3  5792  oqelins4  5794  brfns  5833  qrpprod  5836  fnfullfunlem1  5856  bren  6030  enpw1  6062  brltc  6114  elncs  6119  elnc  6125  ncseqnc  6128  elcan  6329  elscan  6330