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

Step	Hyp	Ref	Expression
1		2falsed.1	. . 3
2	1	pm2.21d 106	. 2
3		2falsed.2	. . 3
4	3	pm2.21d 106	. 2
5	2, 4	impbid 191	1

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