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	⊢ (φ → ψ)
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 341	. 2 ⊢ (¬ ψ → (φ ↔ χ))
5	1, 4	pm2.61i 156	1 ⊢ (φ ↔ χ)

Syntax hints:   → wi 4   ↔ wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  elrabf  2994  sbcco  3069  sbc5  3071  sbcan  3089  sbcor  3091  sbcal  3094  sbcex2  3096  elin  3220  elun  3221  eluni  3895  eliun  3974  el1c  4140  elxpk  4197  eladdc  4399  elopab  4697  opelopabsb  4698  elima  4755  brsi  4762  epelc  4766  opeliunxp  4821  opeliunxp2  4823  br1st  4859  br2nd  4860  brswap2  4861  brco  4884  brcnv  4893  elimasn  5020  opbr1st  5502  opbr2nd  5503  brswap  5510  trtxp  5782  elfix  5788  otelins2  5792  otelins3  5793  oqelins4  5795  brfns  5834  qrpprod  5837  fnfullfunlem1  5857  bren  6031  enpw1  6063  brltc  6115  elncs  6120  elnc  6126  ncseqnc  6129  elcan  6330  elscan  6331