pm2.21 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm2.21 76

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law.

**Assertion**
Ref	Expression
pm2.21

**Proof of Theorem pm2.21**
Step	Hyp	Ref	Expression
1		ax-1 4	. 2
2	1	a3d 75	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

This theorem is referenced by: pm2.24 79 pm2.18 81 peirce 82 nega 84 pm2.5 100 pm3.26im 139 dfor2 229 pm2.42 343 pm5.18 658 mtt 710 mt2bi 711 pm4.82 737 pm5.71 746 dedlem0b 759 dedlemb 761 meredith 921 hbim 1004 ax46to6 1015 ax467to6 1021 ax467to7 1022 hbimd 1106 sbi2 1228 ax11indi 1360 mo 1386 mo2 1393 exmo 1409 2mo 1440 moeq3 1912 opthpr 2476 dvdemo1 2765 ordunisuc2 3105 xrub 6027

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7