MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21ni Unicode version

Theorem pm5.21ni 352
Description: Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypotheses
Ref Expression
pm5.21ni.1
pm5.21ni.2
Assertion
Ref Expression
pm5.21ni

Proof of Theorem pm5.21ni
StepHypRef Expression
1 pm5.21ni.1 . . 3
21con3i 135 . 2
3 pm5.21ni.2 . . 3
43con3i 135 . 2
52, 42falsed 351 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  pm5.21nii  353  norbi  859  pm5.54  902  niabn  951  ordsssuc2  4971  ndmovord  6465  ordsucelsuc  6657  brdomg  7546  suppeqfsuppbi  7863  funsnfsupp  7873  r1pw  8284  r1pwOLD  8285  elixx3g  11571  elfz2  11708  bifald  30486  areaquad  31184
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