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

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
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
21pm2.21d 117 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 117 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 201 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator