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 157 . 2 𝜓 → ¬ 𝜑)
3 pm5.21ni.2 . . 3 (𝜒𝜓)
43con3i 157 . 2 𝜓 → ¬ 𝜒)
52, 42falsed 378 1 𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  pm5.21nii  380  norbi  880  pm5.54  1011  niabn  1014  csbprc  4355  ordsssuc2  6272  ndmovord  7327  ordsucelsuc  7526  brdomg  8507  suppeqfsuppbi  8835  funsnfsupp  8845  r1pw  9262  r1pwALT  9263  elixx3g  12739  elfz2  12887  bifald  35246  areaquad  39701
  Copyright terms: Public domain W3C validator