Theorem pm5.21nii 504

Description: Elimination of antecedent implied by each side of biconditional.

Hypotheses

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

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  eqvinc 1407  elrabf 1421  eldif 1496  elun 1601  elin 1635  eluni 1922  eliun 1998  elopab 2110  opelxp 2452  elxp5 2641  brecop2 3243  sdomsdomcard 3654  elnp 3886  ltresr 4052  hcauchy 5103  sh 5116  closedsub 5128  ch2 5149  h1de2ct 5461  stelt 5671

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org