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

Theorem anass1rs 652
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 468 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 649 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  sossfld  6094  1stconst  7949  infunsdom  9979  creui  11977  qreccl  12718  fsumrlim  15532  fsumo1  15533  climfsum  15541  imasvscaf  17259  grppropd  18603  grpinvpropd  18659  cycsubgcl  18834  frgpup1  19390  ringrghm  19853  phlpropd  20869  mamuass  21558  iccpnfcnv  24116  mbfeqalem1  24814  mbfinf  24838  mbflimsup  24839  mbflimlem  24840  itgfsum  25000  plypf1  25382  mtest  25572  rpvmasum2  26669  ifeqeqx  30894  ordtconnlem1  31883  xrge0iifcnv  31892  fsum2dsub  32596  fvineqsneu  35591  pibt2  35597  incsequz  35915  equivtotbnd  35945  intidl  36196  keridl  36199  prnc  36234  cdleme50trn123  38575  dva1dim  39006  dia1dim2  39083  3factsumint1  40036
  Copyright terms: Public domain W3C validator