Theorem impcon4bid 230

Description: A variation on impbid 215 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)

Hypotheses

Ref	Expression
impcon4bid.1	⊢ (𝜑 → (𝜓 → 𝜒))
impcon4bid.2	⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
impcon4bid	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impcon4bid

Step	Hyp	Ref	Expression
1		impcon4bid.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impcon4bid.2	. . 3 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
3	2	con4d 116	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	impbid 215	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con4bid  320  soisoi  7335  isomin  7344  naddel1  8680  alephdom  10081  nn0n0n1ge2b  12590  om2uzlt2i  14007  sadcaddlem  16539  isprm5  16790  pcdvdsb  16953  om2noseqlt2  28546  expgt0b  33233  oexpreposd  43143  tfsconcatb0  44131  cvgdvgrat  45083  hashnnltb  45792