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 229 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
53, 4impcon4bid 227 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
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 207
This theorem is referenced by:  notbid  318  notbi  319  2falsed  376  had0  1604  cbvexdvaw  2038  cbvexdw  2341  cbvexd  2413  cbvrexdva  3240  raleq  3323  rexeqbidvvOLD  3337  cbvrexdva2  3349  rexeqf  3354  cbvexeqsetf  3495  sbcne12  4415  ordsucuniel  7844  rankr1a  9876  ltaddsub  11737  leaddsub  11739  supxrbnd1  13363  supxrbnd2  13364  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  fllt  13846  rabssnn0fi  14027  elcls  23081  sltrec  27865  rusgrnumwwlks  29994  chrelat3  32390  bj-equsexvwd  36782  wl-sb8eft  37552  wl-sb8et  37554  wl-issetft  37583  infxrbnd2  45380  oddprmne2  47702  nnolog2flm1  48511
  Copyright terms: Public domain W3C validator