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 248 . . 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  2336  cbvexd  2407  rexeqbidvv  3307  cbvrexdva2  3325  vtoclgft  3510  sbcne12  4373  ordsucuniel  7760  rankr1a  9773  ltaddsub  11630  leaddsub  11632  supxrbnd1  13241  supxrbnd2  13242  ioo0  13290  ico0  13311  ioc0  13312  icc0  13313  fllt  13712  rabssnn0fi  13892  elcls  22427  sltrec  27162  rusgrnumwwlks  28922  chrelat3  31316  bj-equsexvwd  35249  wl-sb8et  36011  wl-issetft  36037  infxrbnd2  43610  oddprmne2  45914  nnolog2flm1  46683
  Copyright terms: Public domain W3C validator