MPE Home 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 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  366  bianfd  987  sbcrextOLD  3545  sbcel12  4016  sbcne12  4019  sbcel2  4022  sbcbr  4740  csbxp  5234  smoord  7507  tfr2b  7537  axrepnd  9454  hasheq0  13192  m1exp1  15140  sadcadd  15227  stdbdxmet  22367  iccpnfcnv  22790  cxple2  24488  mirbtwnhl  25620  eupth2lem1  27196  isoun  29607  1smat1  29998  xrge0iifcnv  30107  sgn0bi  30737  signswch  30766  fz0n  31742  hfext  32415  unccur  33522  ntrneiel2  38701  ntrneik4w  38715  eliin2f  39601
  Copyright terms: Public domain W3C validator