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

Theorem 2falsed 351
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 106 . 2
3 2falsed.2 . . 3
43pm2.21d 106 . 2
52, 4impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  pm5.21ni  352  bianfd  926  sbcrext  3410  abvor0  3803  sbcel12  3823  sbcne12  3827  sbcel2  3831  sbcbr123  4503  csbxp  5086  smoord  7055  tfr2b  7084  axrepnd  8990  hasheq0  12433  sadcadd  14108  stdbdxmet  21018  iccpnfcnv  21444  cxple2  23078  mirbtwnhl  24060  uvtx01vtx  24492  eupath2lem1  24977  isoun  27520  xrge0iifcnv  27915  sgn0bi  28486  signswch  28518  fz0n  29110  hfext  29840
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 185
  Copyright terms: Public domain W3C validator