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

Theorem anandi 870
Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
Assertion
Ref Expression
anandi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))

Proof of Theorem anandi
StepHypRef Expression
1 anidm 675 . . 3 ((𝜑𝜑) ↔ 𝜑)
21anbi1i 730 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ (𝜑 ∧ (𝜓𝜒)))
3 an4 864 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
42, 3bitr3i 266 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  anandi3  1050  an3andi  1443  2eu4  2554  inrab  3891  uniin  4448  xpco  5663  fin  6072  fndmin  6310  oaord  7612  nnaord  7684  ixpin  7918  isffth2  16557  fucinv  16614  setcinv  16721  unocv  20005  bldisj  22184  blin  22207  mbfmax  23397  mbfimaopnlem  23403  mbfaddlem  23408  i1faddlem  23441  i1fmullem  23442  lgsquadlem3  25088  numedglnl  26020  wlkeq  26510  ofpreima  29439  ordtconnlem1  29944  dfpo2  31620  fneval  32322  mbfposadd  33428  prtlem70  33958  fz1eqin  37151  fgraphopab  37607  rngcinv  41746  rngcinvALTV  41758  ringcinv  41797  ringcinvALTV  41821
  Copyright terms: Public domain W3C validator