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  4966  ndmovord  6447  ordsucelsuc  6635  brdomg  7523  suppeqfsuppbi  7839  funsnfsupp  7849  r1pw  8259  r1pwOLD  8260  elixx3g  11538  elfz2  11675  bifald  30089  areaquad  30789
  Copyright terms: Public domain W3C validator