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 365
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 148 . 2 𝜓 → ¬ 𝜑)
3 pm5.21ni.2 . . 3 (𝜒𝜓)
43con3i 148 . 2 𝜓 → ¬ 𝜒)
52, 42falsed 364 1 𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  pm5.21nii  366  norbi  899  pm5.54  940  niabn  988  csbprc  3931  ordsssuc2  5717  ndmovord  6699  ordsucelsuc  6891  brdomg  7828  suppeqfsuppbi  8149  funsnfsupp  8159  r1pw  8568  r1pwALT  8569  elixx3g  12015  elfz2  12159  bifald  32854  areaquad  36617
  Copyright terms: Public domain W3C validator