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

Theorem con4bid 318
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 249 . . 3 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 115 . 2 (𝜑 → (𝜓𝜒))
41biimpd 230 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
53, 4impcon4bid 228 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  notbid  319  notbi  320  had0  1590  cbvexd  2387  cbvrexdva2OLD  3411  vtoclgft  3499  sbcne12  4290  ordsucuniel  7402  rankr1a  9118  ltaddsub  10968  leaddsub  10970  supxrbnd1  12568  supxrbnd2  12569  ioo0  12617  ico0  12638  ioc0  12639  icc0  12640  fllt  13030  rabssnn0fi  13208  elcls  21369  rusgrnumwwlks  27439  chrelat3  29835  sltrec  32889  wl-sb8et  34341  infxrbnd2  41199  oddprmne2  43384  nnolog2flm1  44153
  Copyright terms: Public domain W3C validator