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

Theorem bi2.04 247
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 82 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 82 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 125 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imim21b  251  pm4.87  525  imimorbdc  834  sbcom2v  1910  mor  1991  r19.21t  2449  reu8  2812  ra5  2928  unissb  3689  reusv3  4295  zfregfr  4402  tfi  4410  fun11  5094  prime  8906  raluz2  9128  isprm3  11439  isprm4  11440  bj-inf2vnlem2  12139
  Copyright terms: Public domain W3C validator