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 471 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 652 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  sossfld  6012  1stconst  7814  infunsdom  9707  creui  11704  qreccl  12444  fsumrlim  15252  fsumo1  15253  climfsum  15261  imasvscaf  16908  grppropd  18229  grpinvpropd  18285  cycsubgcl  18460  frgpup1  19012  ringrghm  19470  phlpropd  20464  mamuass  21146  iccpnfcnv  23689  mbfeqalem1  24386  mbfinf  24410  mbflimsup  24411  mbflimlem  24412  itgfsum  24571  plypf1  24953  mtest  25143  rpvmasum2  26240  ifeqeqx  30451  ordtconnlem1  31438  xrge0iifcnv  31447  fsum2dsub  32149  fvineqsneu  35194  pibt2  35200  incsequz  35518  equivtotbnd  35548  intidl  35799  keridl  35802  prnc  35837  cdleme50trn123  38180  dva1dim  38611  dia1dim2  38688  3factsumint1  39638
  Copyright terms: Public domain W3C validator