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

Theorem bi2.04 241
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 80 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 80 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 121 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imim21b  245  pm4.87  501  imimorbdc  806  sbcom2v  1877  mor  1958  r19.21t  2411  reu8  2760  ra5  2874  unissb  3638  reusv3  4220  zfregfr  4326  tfi  4333  fun11  4994  prime  8396  raluz2  8618  bj-inf2vnlem2  10483
  Copyright terms: Public domain W3C validator