MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  andi Structured version   Visualization version   GIF version

Theorem andi 1007
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))

Proof of Theorem andi
StepHypRef Expression
1 orc 866 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 867 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 957 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 866 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 618 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 867 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 618 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 856 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 208 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wo 846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847
This theorem is referenced by:  andir  1008  anddi  1010  cadan  1611  indi  4238  indifdirOLD  4250  unrab  4270  uniprOLD  4889  uniun  4896  unopab  5192  xpundi  5705  difxp  6121  coundir  6205  imadif  6590  unpreima  7018  soseq  8096  tpostpos  8182  elznn0nn  12520  faclbnd4lem4  14203  opsrtoslem1  21478  mbfmax  25029  fta1glem2  25547  ofmulrt  25658  lgsquadlem3  26746  nogesgn1o  27037  nosep1o  27045  noinfbnd2lem1  27094  difrab2  31468  ordtconnlem1  32545  ballotlemodife  33137  subfacp1lem6  33819  satf0op  34011  lineunray  34761  wl-ifpimpr  35966  wl-df2-3mintru2  35985  poimirlem30  36137  itg2addnclem2  36159  sticksstones22  40605  lzunuz  41120  diophun  41125  rmydioph  41367  fzunt  41801  fzuntd  41802  fzunt1d  41803  fzuntgd  41804  rp-isfinite6  41864  relexpxpmin  42063  andi3or  42370  clsk1indlem3  42389  simpcntrab  45185  zeoALTV  45936
  Copyright terms: Public domain W3C validator