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

Theorem con4bid 306
 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 237 . . 3 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 113 . 2 (𝜑 → (𝜓𝜒))
41biimpd 218 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
53, 4impcon4bid 216 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  notbid  307  notbi  308  had0  1534  cbvexdva  2271  sbcne12  3938  ordsucuniel  6916  rankr1a  8582  ltaddsub  10381  leaddsub  10383  supxrbnd1  12023  supxrbnd2  12024  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  fllt  12469  rabssnn0fi  12647  elcls  20687  rusgranumwlks  26483  chrelat3  28614  wl-sb8et  32513  infxrbnd2  38526  oddprmne2  40162  rusgrnumwwlks  41177  nnolog2flm1  42182
 Copyright terms: Public domain W3C validator