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

Theorem ancom2s 879
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 464 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 492 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  an42s  905  sotr2  5216  somin2  5689  f1elima  6684  f1imaeq  6686  soisoi  6742  isosolem  6761  xpexr2  7273  2ndconst  7435  smoword  7633  unxpdomlem3  8333  fiming  8571  fiinfg  8572  sornom  9311  fin1a2s  9448  mulsub  10685  leltadd  10724  ltord1  10766  leord1  10767  eqord1  10768  divmul24  10941  expcan  13127  ltexp2  13128  fsum  14670  fprod  14890  isprm5  15641  ramub  15939  setcinv  16961  grpidpropd  17482  gsumpropd2lem  17494  cmnpropd  18422  unitpropd  18917  lidl1el  19440  gsumcom3  20427  1marepvmarrepid  20603  1marepvsma1  20611  ordtrest2  21230  filuni  21910  haustsms2  22161  blcomps  22419  blcom  22420  metnrmlem3  22885  cnmpt2pc  22948  icoopnst  22959  icccvx  22970  equivcfil  23317  volcn  23594  dvmptfsum  23957  cxple  24661  cxple3  24667  uhgr2edg  26320  lnosub  27944  chirredlem2  29580  bhmafibid2  29975  metider  30267  ordtrest2NEW  30299  fsum2dsub  31015  finxpreclem2  33556  fin2so  33727  cover2  33839  filbcmb  33866  isdrngo2  34088  crngohomfo  34136  unichnidl  34161  cdleme50eq  36349  dvhvaddcomN  36905  ismrc  37784
  Copyright terms: Public domain W3C validator