Theorem pm5.21nii 678

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

Hypotheses

Ref	Expression
pm5.21ni.1	⊢ (φ → ψ)
pm5.21ni.2	⊢ (χ → ψ)
pm5.21nii.3	⊢ (ψ → (φ ↔ χ))

Assertion

Ref	Expression
pm5.21nii	⊢ (φ ↔ χ)

Proof of Theorem pm5.21nii

Step	Hyp	Ref	Expression
1		pm5.21nii.3	. 2 ⊢ (ψ → (φ ↔ χ))
2		pm5.21ni.1	. . 3 ⊢ (φ → ψ)
3		pm5.21ni.2	. . 3 ⊢ (χ → ψ)
4	2, 3	pm5.21ni 677	. 2 ⊢ (¬ ψ → (φ ↔ χ))
5	1, 4	pm2.61i 126	1 ⊢ (φ ↔ χ)

Syntax hints:   → wi 3   ↔ wb 146

This theorem is referenced by:  eqvinc 1879  elrabf 1900  eldif 2053  elun 2169  elin 2203  eluni 2501  eliun 2565  elopab 2806  elpwun 2906  opelxp 3209  elxp5 3446  brecop2 4297  card1 4813  sdomsdomcard 4828  elnp 5072  ltresr 5238  dfuz 6158  eluz2t 6361  eltopsp 7554  tpsex 7555  istps 7556  isvc 8152  isnv 8183  hcau 8990  sh 9017  closedsub 9032  ch2 9053  h1de2ct 9418  elcnopt 9723  ellnopt 9724  elunopt 9739  elhmopt 9740  elcnfnt 9749  ellnfnt 9750  stelt 10079  hstelt 10080  elsymgrn 10335

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