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

Theorem pm5.21ni 379
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 154 . 2 𝜓 → ¬ 𝜑)
3 pm5.21ni.2 . . 3 (𝜒𝜓)
43con3i 154 . 2 𝜓 → ¬ 𝜒)
52, 42falsed 377 1 𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  pm5.21nii  380  norbi  886  pm5.54  1017  niabn  1020  ab0w  4374  csbprc  4407  ralf0  4514  ordsssuc2  6456  ndmovord  7597  ordsucelsuc  7810  brdomg  8952  brdomgOLD  8953  suppeqfsuppbi  9377  funsnfsupp  9387  r1pw  9840  r1pwALT  9841  elixx3g  13337  elfz2  13491  bifald  36955  areaquad  41965
  Copyright terms: Public domain W3C validator