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

Theorem pm5.21ni 350
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  |-  ( ph  ->  ps )
pm5.21ni.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
pm5.21ni  |-  ( -. 
ps  ->  ( ph  <->  ch )
)

Proof of Theorem pm5.21ni
StepHypRef Expression
1 pm5.21ni.1 . . 3  |-  ( ph  ->  ps )
21con3i 135 . 2  |-  ( -. 
ps  ->  -.  ph )
3 pm5.21ni.2 . . 3  |-  ( ch 
->  ps )
43con3i 135 . 2  |-  ( -. 
ps  ->  -.  ch )
52, 42falsed 349 1  |-  ( -. 
ps  ->  ( ph  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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
This theorem is referenced by:  pm5.21nii  351  norbi  857  pm5.54  900  niabn  949  ordsssuc2  4893  ndmovord  6382  ordsucelsuc  6574  brdomg  7463  suppeqfsuppbi  7776  funsnfsupp  7786  r1pw  8194  r1pwALT  8195  elixx3g  11481  elfz2  11618  bifald  30688  areaquad  31388
  Copyright terms: Public domain W3C validator