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 376
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 375 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  377  norbi  883  pm5.54  1014  niabn  1017  ab0w  4372  csbprc  4405  ralf0  4512  ordsssuc2  6454  ndmovord  7599  ordsucelsuc  7812  brdomg  8954  brdomgOLD  8955  suppeqfsuppbi  9379  funsnfsupp  9389  r1pw  9842  r1pwALT  9843  elixx3g  13341  elfz2  13495  bifald  37258  areaquad  42267
  Copyright terms: Public domain W3C validator