Theorem 2falsed 366

Description: Two falsehoods are equivalent (deduction rule). (Contributed by NM, 11-Oct-2013.)

Hypotheses

Ref	Expression
2falsed.1	⊢ (𝜑 → ¬ 𝜓)
2falsed.2	⊢ (𝜑 → ¬ 𝜒)

Assertion

Ref	Expression
2falsed	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem 2falsed

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	pm2.21d 118	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 118	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 202	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  pm5.21ni  367  bianfd  967  sbcrextOLD  3512  sbcel12  3983  sbcne12  3986  sbcel2  3989  sbcbr  4707  csbxp  5200  smoord  7462  tfr2b  7492  axrepnd  9416  hasheq0  13154  m1exp1  15093  sadcadd  15180  stdbdxmet  22320  iccpnfcnv  22743  cxple2  24443  mirbtwnhl  25575  uvtxa01vtx  26298  eupth2lem1  27078  isoun  29479  1smat1  29870  xrge0iifcnv  29979  sgn0bi  30609  signswch  30638  fz0n  31616  hfext  32290  unccur  33392  ntrneiel2  38384  ntrneik4w  38398  eliin2f  39287