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

Theorem con4bid 316
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  317  notbi  318  2falsed  375  had0  1598  cbvexdvaw  2035  cbvexdw  2330  cbvexd  2402  cbvrexdva  3228  raleq  3312  rexeqbidvvOLD  3322  cbvrexdva2  3333  rexeqf  3338  issetft  3477  sbcne12  4417  ordsucuniel  7833  rankr1a  9879  ltaddsub  11738  leaddsub  11740  supxrbnd1  13354  supxrbnd2  13355  ioo0  13403  ico0  13424  ioc0  13425  icc0  13426  fllt  13826  rabssnn0fi  14006  elcls  23068  sltrec  27850  rusgrnumwwlks  29908  chrelat3  32304  bj-equsexvwd  36486  wl-sb8eft  37246  wl-sb8et  37248  wl-issetft  37277  infxrbnd2  44984  oddprmne2  47287  nnolog2flm1  47978
  Copyright terms: Public domain W3C validator