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

Theorem impcon4bid 227
Description: A variation on impbid 212 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)
Hypotheses
Ref Expression
impcon4bid.1 (𝜑 → (𝜓𝜒))
impcon4bid.2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
Assertion
Ref Expression
impcon4bid (𝜑 → (𝜓𝜒))

Proof of Theorem impcon4bid
StepHypRef Expression
1 impcon4bid.1 . 2 (𝜑 → (𝜓𝜒))
2 impcon4bid.2 . . 3 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
32con4d 115 . 2 (𝜑 → (𝜒𝜓))
41, 3impbid 212 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:  con4bid  317  soisoi  7348  isomin  7357  naddel1  8724  alephdom  10119  nn0n0n1ge2b  12593  om2uzlt2i  13989  sadcaddlem  16491  isprm5  16741  pcdvdsb  16903  om2noseqlt2  28321  expgt0b  32823  oexpreposd  42336  tfsconcatb0  43334  cvgdvgrat  44309
  Copyright terms: Public domain W3C validator