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  5503  somin2  5992  f1elima  7018  f1imaeq  7020  soisoi  7076  isosolem  7095  xpexr2  7615  smoword  7997  unxpdomlem3  8716  fiming  8954  fiinfg  8955  sornom  9691  fin1a2s  9828  mul4r  10801  mulsub  11075  leltadd  11116  ltord1  11158  leord1  11159  eqord1  11160  divmul24  11336  expcan  13526  ltexp2  13527  bhmafibid2  14819  fsum  15069  fprod  15287  isprm5  16043  ramub  16341  setcinv  17342  grpidpropd  17863  gsumpropd2lem  17880  cmnpropd  18838  gsumcom3  19020  unitpropd  19369  lidl1el  19912  1marepvmarrepid  21102  1marepvsma1  21110  ordtrest2  21730  filuni  22411  haustsms2  22662  blcomps  22920  blcom  22921  metnrmlem3  23386  cnmpopc  23449  icoopnst  23460  icccvx  23471  equivcfil  23819  volcn  24124  dvmptfsum  24489  cxple  25193  cxple3  25199  uhgr2edg  26906  lnosub  28452  chirredlem2  30084  metider  31022  ordtrest2NEW  31054  fsum2dsub  31766  finxpreclem2  34542  fin2so  34748  cover2  34859  filbcmb  34885  isdrngo2  35106  crngohomfo  35154  unichnidl  35179  cdleme50eq  37546  dvhvaddcomN  38101  ismrc  39165  prproropf1olem4  43502
  Copyright terms: Public domain W3C validator