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  1005  sbcrextOLD  3645  sbcel12  4118  sbcne12  4121  sbcel2  4124  sbcbr  4851  csbxp  5349  smoord  7623  tfr2b  7653  axrepnd  9600  hasheq0  13338  m1exp1  15287  sadcadd  15374  stdbdxmet  22513  iccpnfcnv  22936  cxple2  24634  mirbtwnhl  25766  eupth2lem1  27362  isoun  29780  1smat1  30171  xrge0iifcnv  30280  sgn0bi  30910  signswch  30939  fz0n  31915  hfext  32588  unccur  33697  ntrneiel2  38878  ntrneik4w  38892  eliin2f  39778
  Copyright terms: Public domain W3C validator