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

Theorem 2falsed 366
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 118 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 118 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 202 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  pm5.21ni  367  bianfd  966  sbcrextOLD  3499  sbcel12  3961  sbcne12  3964  sbcel2  3967  sbcbr  4677  csbxp  5171  smoord  7422  tfr2b  7452  axrepnd  9376  hasheq0  13110  m1exp1  15036  sadcadd  15123  stdbdxmet  22260  iccpnfcnv  22683  cxple2  24377  mirbtwnhl  25509  uvtxa01vtx  26219  eupth2lem1  26978  isoun  29363  1smat1  29694  xrge0iifcnv  29803  sgn0bi  30432  signswch  30460  fz0n  31377  hfext  31985  unccur  33063  ntrneiel2  37905  ntrneik4w  37919  eliin2f  38809
  Copyright terms: Public domain W3C validator