MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.21ni Structured version   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  |-  ( 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 351 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  353  norbi  857  pm5.54  900  niabn  949  ordsssuc2  4953  ndmovord  6447  ordsucelsuc  6639  brdomg  7525  suppeqfsuppbi  7842  funsnfsupp  7852  r1pw  8263  r1pwOLD  8264  elixx3g  11548  elfz2  11685  bifald  30458  areaquad  31157
  Copyright terms: Public domain W3C validator