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

Theorem anass1rs 651
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 466 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 648 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  sossfld  6184  1stconst  8088  infunsdom  10211  creui  12211  qreccl  12957  fsumrlim  15761  fsumo1  15762  climfsum  15770  imasvscaf  17489  grppropd  18873  grpinvpropd  18934  cycsubgcl  19121  frgpup1  19684  ringrghm  20201  phlpropd  21427  mamuass  22122  iccpnfcnv  24689  mbfeqalem1  25390  mbfinf  25414  mbflimsup  25415  mbflimlem  25416  itgfsum  25576  plypf1  25961  mtest  26152  rpvmasum2  27251  ifeqeqx  32041  ordtconnlem1  33202  xrge0iifcnv  33211  fsum2dsub  33917  fvineqsneu  36595  pibt2  36601  incsequz  36919  equivtotbnd  36949  intidl  37200  keridl  37203  prnc  37238  cdleme50trn123  39728  dva1dim  40159  dia1dim2  40236  3factsumint1  41192
  Copyright terms: Public domain W3C validator