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 377
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 376 1 𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
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 207
This theorem is referenced by:  pm5.21nii  378  norbi  886  pm5.54  1019  niabn  1022  sbccomlem  3878  ab0w  4385  csbprc  4415  ralf0  4520  ordsssuc2  6477  ndmovord  7623  ordsucelsuc  7842  brdomg  8996  brdomgOLD  8997  suppeqfsuppbi  9417  funsnfsupp  9430  r1pw  9883  r1pwALT  9884  elixx3g  13397  elfz2  13551  bifald  38074  areaquad  43205
  Copyright terms: Public domain W3C validator