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  8725  alephdom  10121  nn0n0n1ge2b  12595  om2uzlt2i  13992  sadcaddlem  16494  isprm5  16744  pcdvdsb  16907  om2noseqlt2  28306  expgt0b  32818  oexpreposd  42357  tfsconcatb0  43357  cvgdvgrat  44332
  Copyright terms: Public domain W3C validator