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  376  had0  1605  cbvexdvaw  2042  cbvexdw  2335  cbvexd  2406  cbvrexdva  3236  raleq  3321  rexeqbidvvOLD  3331  cbvrexdva2  3344  rexeqf  3349  vtoclgft  3537  sbcne12  4408  ordsucuniel  7795  rankr1a  9813  ltaddsub  11670  leaddsub  11672  supxrbnd1  13282  supxrbnd2  13283  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  fllt  13753  rabssnn0fi  13933  elcls  22506  sltrec  27247  rusgrnumwwlks  29093  chrelat3  31487  bj-equsexvwd  35463  wl-sb8et  36222  wl-issetft  36248  infxrbnd2  43852  oddprmne2  46155  nnolog2flm1  46924
  Copyright terms: Public domain W3C validator