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

Theorem 2falsed 380
 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 268 . 2 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
43con4bid 320 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  pm5.21ni  382  bianfd  538  sbcel12  4316  sbcne12  4320  sbcel2  4323  sbcbr  5085  csbxp  5614  smoord  7987  tfr2b  8017  axrepnd  10007  hasheq0  13722  m1exp1  15719  sadcadd  15799  stdbdxmet  23129  iccpnfcnv  23556  cxple2  25295  mirbtwnhl  26481  eupth2lem1  28010  isoun  30468  1smat1  31169  xrge0iifcnv  31298  sgn0bi  31927  signswch  31953  fmlafvel  32757  fz0n  33087  hfext  33769  unccur  35056  ntrneiel2  40804  ntrneik4w  40818  eliin2f  41755
 Copyright terms: Public domain W3C validator