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

Theorem anass1rs 634
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 453 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 631 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  sossfld  5720  infunsdom  9242  creui  11221  qreccl  12016  fsumrlim  14750  fsumo1  14751  climfsum  14759  imasvscaf  16407  grppropd  17645  grpinvpropd  17698  cycsubgcl  17828  frgpup1  18395  ringrghm  18813  phlpropd  20217  mamuass  20425  iccpnfcnv  22963  mbfeqalem  23629  mbfinf  23652  mbflimsup  23653  mbflimlem  23654  itgfsum  23813  plypf1  24188  mtest  24378  rpvmasum2  25422  ifeqeqx  29699  ordtconnlem1  30310  xrge0iifcnv  30319  fsum2dsub  31025  incsequz  33876  equivtotbnd  33909  intidl  34160  keridl  34163  prnc  34198  cdleme50trn123  36364  dva1dim  36795  dia1dim2  36872
  Copyright terms: Public domain W3C validator