Theorem pm5.21nii 679

Description: Eliminate an antecedent implied by each side of a biconditional.

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 678	. 2 |- (-. ps -> (ph <-> ch))
5	1, 4	pm2.61i 126	1 |- (ph <-> ch)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  eqvinc 1883  elrabf 1904  eldif 2057  elun 2173  elin 2207  eluni 2506  eliun 2570  elopab 2811  elpwun 2911  opelxp 3214  elxp5 3454  brecop2 4307  card1 4833  sdomsdomcard 4848  elnp 5092  ltresr 5258  dfuz 6202  eluz2t 6421  eltopsp 7604  tpsex 7605  istps 7606  isvc 8200  isnv 8231  hcau 9051  sh 9078  closedsub 9093  ch2 9114  h1de2ct 9479  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  stelt 10141  hstelt 10142  elsymgrn 10401

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain