MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2falsed Structured version   Visualization version   GIF version

Theorem 2falsed 375
Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) (Proof shortened by Wolf Lammen, 11-Apr-2024.)
Hypotheses
Ref Expression
2falsed.1 (𝜑 → ¬ 𝜓)
2falsed.2 (𝜑 → ¬ 𝜒)
Assertion
Ref Expression
2falsed (𝜑 → (𝜓𝜒))

Proof of Theorem 2falsed
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
2 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
31, 22thd 264 . 2 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
43con4bid 316 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  pm5.21ni  376  bianfd  533  sbcel12  4410  sbcne12  4414  sbcel2  4417  sbcbr  5205  csbxp  5779  smoord  8390  tfr2b  8421  axrepnd  10623  hasheq0  14360  m1exp1  16358  sadcadd  16438  stdbdxmet  24442  iccpnfcnv  24887  cxple2  26649  mirbtwnhl  28502  eupth2lem1  30046  ifnebib  32358  isoun  32499  1smat1  33410  xrge0iifcnv  33539  sgn0bi  34172  signswch  34198  fmlafvel  35000  fz0n  35330  hfext  35784  unccur  37081  ntrneiel2  43519  ntrneik4w  43533  eliin2f  44473
  Copyright terms: Public domain W3C validator