Theorem pm5.21nii 676

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 675	. 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 1855  elrabf 1876  eldif 2028  elun 2144  elin 2178  eluni 2474  eliun 2538  elopab 2773  elpwun 2874  opelxp 3176  elxp5 3403  brecop2 4245  sdomsdomcard 4771  elnp 5015  ltresr 5181  dfuz 6101  eluz2t 6304  eltopsp 7497  tpsex 7498  istps 7499  elsymgrn 8668  hcau 9201  sh 9229  closedsub 9244  ch2 9265  h1de2ct 9609  elcnopt 9914  ellnopt 9915  elunopt 9930  elhmopt 9931  elcnfnt 9940  ellnfnt 9941  stelt 10265  hstelt 10266

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