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

Theorem anandi 826
Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
Assertion
Ref Expression
anandi  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )

Proof of Theorem anandi
StepHypRef Expression
1 anidm 644 . . 3  |-  ( (
ph  /\  ph )  <->  ph )
21anbi1i 695 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ph  /\  ( ps  /\  ch ) ) )
3 an4 822 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
42, 3bitr3i 251 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ph  /\  ps )  /\  ( ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anandi3  987  an3andi  1341  2eu4  2390  inrab  3775  uniin  4271  xpco  5553  fin  5771  fndmin  5995  oaord  7208  nnaord  7280  ixpin  7506  isffth2  15160  fucinv  15217  setcinv  15292  unocv  18580  bldisj  20769  blin  20792  mbfmax  21924  mbfimaopnlem  21930  mbfaddlem  21935  i1faddlem  21968  i1fmullem  21969  lgsquadlem3  23497  2wlkeq  24530  ofpreima  27330  ordtconlem1  27731  dfpo2  29111  mbfposadd  29989  fneval  30097  prtlem70  30520  fz1eqin  30630  fgraphopab  31099  ringcinv  32372
  Copyright terms: Public domain W3C validator