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  7337  isomin  7346  naddel1  8698  alephdom  10161  nn0n0n1ge2b  12676  om2uzlt2i  14095  sadcaddlem  16628  isprm5  16884  pcdvdsb  17048  om2noseqlt2  28687  expgt0b  33409  oexpreposd  43381  tfsconcatb0  44347  cvgdvgrat  45298  hashnnltb  46014