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

Theorem fal 1459
 Description: The truth value is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
Assertion
Ref Expression
fal

Proof of Theorem fal
StepHypRef Expression
1 tru 1456 . . 3
21notnoti 127 . 2
3 df-fal 1458 . 2
42, 3mtbir 306 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wtru 1453   wfal 1457 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 190  df-tru 1455  df-fal 1458 This theorem is referenced by:  nbfal  1463  bifal  1465  falim  1466  dfnot  1470  falantru  1476  notfal  1487  nffal  1688  nonconne  2655  csbprc  3774  axnulALT  4524  axnul  4525  canthp1  9097  rlimno1  13794  1stccnp  20554  rusgra0edg  25762  alnof  31133  nextf  31137  negsym1  31148  nandsym1  31153  subsym1  31158  bj-falor  31232  bj-nffal  31265  orfa  32379  fald  32435  dihglblem6  34979  ifpdfan  36180  ifpnot  36184  ifpid2  36185  ifpdfxor  36202
 Copyright terms: Public domain W3C validator