Theorem 2falsed 365

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 117	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		2falsed.2	. . 3 ⊢ (𝜑 → ¬ 𝜒)
4	3	pm2.21d 117	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
5	2, 4	impbid 201	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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 196

This theorem is referenced by:  pm5.21ni  366  bianfd  963  sbcrextOLD  3479  sbcel12  3935  sbcne12  3938  sbcel2  3941  sbcbr  4637  csbxp  5123  smoord  7349  tfr2b  7379  axrepnd  9295  hasheq0  13015  m1exp1  14931  sadcadd  15018  stdbdxmet  22130  iccpnfcnv  22551  cxple2  24243  mirbtwnhl  25375  uvtx01vtx  26020  eupath2lem1  26504  isoun  28862  1smat1  29198  xrge0iifcnv  29307  sgn0bi  29936  signswch  29964  fz0n  30869  hfext  31460  unccur  32562  ntrneiel2  37404  ntrneik4w  37418  uvtxa01vtx  40624  eupth2lem1  41386