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

Theorem 2falsed 364
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
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
21pm2.21d 116 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 116 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 200 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  pm5.21ni  365  bianfd  962  sbcrextOLD  3474  sbcel12  3930  sbcne12  3933  sbcel2  3936  sbcbr  4627  csbxp  5109  smoord  7322  tfr2b  7352  axrepnd  9268  hasheq0  12963  m1exp1  14873  sadcadd  14960  stdbdxmet  22067  iccpnfcnv  22478  cxple2  24156  mirbtwnhl  25289  uvtx01vtx  25782  eupath2lem1  26266  isoun  28664  1smat1  29000  xrge0iifcnv  29109  sgn0bi  29738  signswch  29766  fz0n  30671  hfext  31262  unccur  32361  ntrneiel2  37203  ntrneik4w  37217  uvtxa01vtx  40622  eupth2lem1  41384
  Copyright terms: Public domain W3C validator