MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con4bid Structured version   Visualization version   GIF version

Theorem con4bid 317
Description: A contraposition deduction. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
con4bid.1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Assertion
Ref Expression
con4bid (𝜑 → (𝜓𝜒))

Proof of Theorem con4bid
StepHypRef Expression
1 con4bid.1 . . . 4 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
21biimprd 247 . . 3 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 115 . 2 (𝜑 → (𝜓𝜒))
41biimpd 228 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
53, 4impcon4bid 226 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:  notbid  318  notbi  319  2falsed  377  had0  1606  cbvexdvaw  2043  cbvexdw  2337  cbvexd  2409  rexeqbidvv  3340  vtoclgft  3493  sbcne12  4347  ordsucuniel  7680  rankr1a  9603  ltaddsub  11458  leaddsub  11460  supxrbnd1  13064  supxrbnd2  13065  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  fllt  13535  rabssnn0fi  13715  elcls  22233  rusgrnumwwlks  28348  chrelat3  30742  sltrec  34023  bj-equsexvwd  34972  wl-sb8et  35717  infxrbnd2  42915  oddprmne2  45178  nnolog2flm1  45947
  Copyright terms: Public domain W3C validator