ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bi2.04 GIF version

Theorem bi2.04 237
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
bi2.04 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 76 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 76 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 117 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  imim21b  241  pm4.87  493  imimorbdc  795  sbcom2v  1861  mor  1942  r19.21t  2394  reu8  2737  ra5  2846  unissb  3610  reusv3  4192  zfregfr  4298  tfi  4305  fun11  4966  prime  8337  raluz2  8522  bj-inf2vnlem2  10096
  Copyright terms: Public domain W3C validator