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

Theorem anass1rs 646
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 460 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 643 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  sossfld  5797  1stconst  7502  infunsdom  9324  creui  11307  qreccl  12053  fsumrlim  14881  fsumo1  14882  climfsum  14890  imasvscaf  16514  grppropd  17753  grpinvpropd  17806  cycsubgcl  17933  frgpup1  18503  ringrghm  18921  phlpropd  20324  mamuass  20533  iccpnfcnv  23071  mbfeqalem1  23749  mbfinf  23773  mbflimsup  23774  mbflimlem  23775  itgfsum  23934  plypf1  24309  mtest  24499  rpvmasum2  25553  ifeqeqx  29879  ordtconnlem1  30486  xrge0iifcnv  30495  fsum2dsub  31205  incsequz  34031  equivtotbnd  34064  intidl  34315  keridl  34318  prnc  34353  cdleme50trn123  36575  dva1dim  37006  dia1dim2  37083
  Copyright terms: Public domain W3C validator