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

Theorem 2falsed 341
 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 100 . 2
3 2falsed.2 . . 3
43pm2.21d 100 . 2
52, 4impbid 184 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177 This theorem is referenced by:  pm5.21ni  342  bianfd  893  abvor0  3637  smoord  6619  tfr2b  6649  axrepnd  8459  hasheq0  11634  sadcadd  12960  stdbdxmet  18535  iccpnfcnv  18959  cxple2  20578  uvtx01vtx  21491  eupath2lem1  21689  isoun  24079  xrge0iifcnv  24309  fz0n  25192  hfext  26089 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178
 Copyright terms: Public domain W3C validator