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

Theorem ancom2s 646
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
an12s.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
ancom2s ((𝜑 ∧ (𝜒𝜓)) → 𝜃)

Proof of Theorem ancom2s
StepHypRef Expression
1 pm3.22 460 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 592 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  an42s  657  sotr2  5499  somin2  5989  f1elima  7012  f1imaeq  7014  soisoi  7070  isosolem  7089  xpexr2  7612  smoword  7994  unxpdomlem3  8713  fiming  8951  fiinfg  8952  sornom  9688  fin1a2s  9825  mul4r  10798  mulsub  11072  leltadd  11113  ltord1  11155  leord1  11156  eqord1  11157  divmul24  11333  expcan  13523  ltexp2  13524  bhmafibid2  14816  fsum  15067  fprod  15285  isprm5  16041  ramub  16339  setcinv  17340  grpidpropd  17862  gsumpropd2lem  17879  cmnpropd  18847  gsumcom3  19029  unitpropd  19378  lidl1el  19921  1marepvmarrepid  21114  1marepvsma1  21122  ordtrest2  21742  filuni  22423  haustsms2  22674  blcomps  22932  blcom  22933  metnrmlem3  23398  cnmpopc  23461  icoopnst  23472  icccvx  23483  equivcfil  23831  volcn  24136  dvmptfsum  24501  cxple  25205  cxple3  25211  uhgr2edg  26918  lnosub  28464  chirredlem2  30096  metider  31034  ordtrest2NEW  31066  fsum2dsub  31778  finxpreclem2  34554  fin2so  34761  cover2  34872  filbcmb  34898  isdrngo2  35119  crngohomfo  35167  unichnidl  35192  cdleme50eq  37559  dvhvaddcomN  38114  ismrc  39178  prproropf1olem4  43515
  Copyright terms: Public domain W3C validator