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  855  pm5.54  895  niabn  942  ordsssuc2  4908  ndmovord  6356  ordsucelsuc  6536  brdomg  7423  suppeqfsuppbi  7738  funsnfsupp  7748  r1pw  8156  r1pwOLD  8157  elixx3g  11417  elfz2  11554  bifald  29030  areaquad  29733
  Copyright terms: Public domain W3C validator