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

Theorem andi 730
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 632 . . 3 ((φ ψ) → ((φ ψ) (φ χ)))
2 olc 631 . . 3 ((φ χ) → ((φ ψ) (φ χ)))
31, 2jaodan 709 . 2 ((φ (ψ χ)) → ((φ ψ) (φ χ)))
4 orc 632 . . . 4 (ψ → (ψ χ))
54anim2i 324 . . 3 ((φ ψ) → (φ (ψ χ)))
6 olc 631 . . . 4 (χ → (ψ χ))
76anim2i 324 . . 3 ((φ χ) → (φ (ψ χ)))
85, 7jaoi 635 . 2 (((φ ψ) (φ χ)) → (φ (ψ χ)))
93, 8impbii 117 1 ((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  andir  731  anddi  733  dcim  783  dcan  841  excxor  1268  sbequilem  1716  sborv  1767  r19.43  2462  indi  3178  difindiss  3185  unrab  3202  unipr  3585  uniun  3590  unopab  3827  xpundi  4339  coundir  4766  unpreima  5235  tpostpos  5820  elni2  6298  elznn0nn  7995
  Copyright terms: Public domain W3C validator