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 467 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 652 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  sossfld  6133  1stconst  8030  infunsdom  10104  creui  12120  qreccl  12867  fsumrlim  15718  fsumo1  15719  climfsum  15727  imasvscaf  17443  grppropd  18864  grpinvpropd  18928  cycsubgcl  19118  frgpup1  19687  ringrghm  20231  phlpropd  21592  mamuass  22317  iccpnfcnv  24869  mbfeqalem1  25569  mbfinf  25593  mbflimsup  25594  mbflimlem  25595  itgfsum  25755  plypf1  26144  mtest  26340  rpvmasum2  27450  ifeqeqx  32522  ordtconnlem1  33937  xrge0iifcnv  33946  fsum2dsub  34620  fvineqsneu  37455  pibt2  37461  incsequz  37787  equivtotbnd  37817  intidl  38068  keridl  38071  prnc  38106  cdleme50trn123  40652  dva1dim  41083  dia1dim2  41160  3factsumint1  42113  modelac8prim  45084
  Copyright terms: Public domain W3C validator