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

Theorem anass1rs 655
Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
anass1rs.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
anass1rs (((𝜑𝜒) ∧ 𝜓) → 𝜃)

Proof of Theorem anass1rs
StepHypRef Expression
1 anass1rs.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21anassrs 467 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 652 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  sossfld  6144  1stconst  8042  infunsdom  10123  creui  12140  qreccl  12882  fsumrlim  15734  fsumo1  15735  climfsum  15743  imasvscaf  17460  grppropd  18881  grpinvpropd  18945  cycsubgcl  19135  frgpup1  19704  ringrghm  20248  phlpropd  21610  mamuass  22346  iccpnfcnv  24898  mbfeqalem1  25598  mbfinf  25622  mbflimsup  25623  mbflimlem  25624  itgfsum  25784  plypf1  26173  mtest  26369  rpvmasum2  27479  ifeqeqx  32617  ordtconnlem1  34081  xrge0iifcnv  34090  fsum2dsub  34764  regsfromregtr  36668  fvineqsneu  37616  pibt2  37622  incsequz  37949  equivtotbnd  37979  intidl  38230  keridl  38233  prnc  38268  cdleme50trn123  40814  dva1dim  41245  dia1dim2  41322  3factsumint1  42275  modelac8prim  45233
  Copyright terms: Public domain W3C validator