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

Theorem andi 719
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi ((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))

Proof of Theorem andi
StepHypRef Expression
1 orc 620 . . 3 ((φ ψ) → ((φ ψ) (φ χ)))
2 olc 619 . . 3 ((φ χ) → ((φ ψ) (φ χ)))
31, 2jaodan 697 . 2 ((φ (ψ χ)) → ((φ ψ) (φ χ)))
4 orc 620 . . . 4 (ψ → (ψ χ))
54anim2i 324 . . 3 ((φ ψ) → (φ (ψ χ)))
6 olc 619 . . . 4 (χ → (ψ χ))
76anim2i 324 . . 3 ((φ χ) → (φ (ψ χ)))
85, 7jaoi 623 . 2 (((φ ψ) (φ χ)) → (φ (ψ χ)))
93, 8impbii 117 1 ((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   wo 616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  andir  720  anddi  722  dcim  772  dcan  828  excxor  1252  sbequilem  1697  sborv  1748  r19.43  2442  indi  3157  difindiss  3164  unrab  3181  unipr  3564  uniun  3569  unopab  3806  xpundi  4319  coundir  4746  unpreima  5213  tpostpos  5797  elni2  6168
  Copyright terms: Public domain W3C validator