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

Theorem anass1rs 653
 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 470 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
32an32s 650 1 (((𝜑𝜒) ∧ 𝜓) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  sossfld  6036  1stconst  7787  infunsdom  9628  creui  11625  qreccl  12360  fsumrlim  15158  fsumo1  15159  climfsum  15167  imasvscaf  16804  grppropd  18110  grpinvpropd  18166  cycsubgcl  18341  frgpup1  18893  ringrghm  19347  phlpropd  20791  mamuass  21003  iccpnfcnv  23540  mbfeqalem1  24234  mbfinf  24258  mbflimsup  24259  mbflimlem  24260  itgfsum  24419  plypf1  24794  mtest  24984  rpvmasum2  26080  ifeqeqx  30289  ordtconnlem1  31155  xrge0iifcnv  31164  fsum2dsub  31866  fvineqsneu  34674  pibt2  34680  incsequz  35005  equivtotbnd  35038  intidl  35289  keridl  35292  prnc  35327  cdleme50trn123  37672  dva1dim  38103  dia1dim2  38180
 Copyright terms: Public domain W3C validator