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  4334  csbprc  4367  ralf0  4472  ordsssuc2  6409  ndmovord  7545  ordsucelsuc  7758  brdomg  8897  brdomgOLD  8898  suppeqfsuppbi  9320  funsnfsupp  9330  r1pw  9782  r1pwALT  9783  elixx3g  13278  elfz2  13432  bifald  36549  areaquad  41553
  Copyright terms: Public domain W3C validator