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

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

Proof of Theorem 2falsed
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
21pm2.21d 121 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 121 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 213 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  pm5.21ni  379  bianfd  535  sbcel12  4284  sbcne12  4288  sbcel2  4291  sbcbr  5021  csbxp  5541  smoord  7859  tfr2b  7889  axrepnd  9867  hasheq0  13579  m1exp1  15565  sadcadd  15645  stdbdxmet  22813  iccpnfcnv  23236  cxple2  24966  mirbtwnhl  26153  eupth2lem1  27690  isoun  30130  1smat1  30689  xrge0iifcnv  30798  sgn0bi  31427  signswch  31453  fmlafvel  32247  fz0n  32577  hfext  33260  unccur  34432  ntrneiel2  39947  ntrneik4w  39961  eliin2f  40936
  Copyright terms: Public domain W3C validator