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

Theorem con4bid 320
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 251 . . 3 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 115 . 2 (𝜑 → (𝜓𝜒))
41biimpd 232 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
53, 4impcon4bid 230 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  notbid  321  notbi  322  2falsed  380  had0  1610  cbvexdvaw  2051  cbvexdw  2342  cbvexd  2409  rexeqbidvv  3308  vtoclgft  3460  sbcne12  4312  ordsucuniel  7570  rankr1a  9350  ltaddsub  11204  leaddsub  11206  supxrbnd1  12809  supxrbnd2  12810  ioo0  12858  ico0  12879  ioc0  12880  icc0  12881  fllt  13279  rabssnn0fi  13457  elcls  21836  rusgrnumwwlks  27924  chrelat3  30318  sltrec  33669  bj-equsexvwd  34618  wl-sb8et  35363  infxrbnd2  42486  oddprmne2  44748  nnolog2flm1  45517
  Copyright terms: Public domain W3C validator