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

Theorem ancom2s 839
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 463 . 2 ((𝜒𝜓) → (𝜓𝜒))
2 an12s.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 489 1 ((𝜑 ∧ (𝜒𝜓)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  an42s  865  sotr2  4977  somin2  5436  f1elima  6398  f1imaeq  6400  soisoi  6455  isosolem  6474  xpexr2  6977  2ndconst  7130  smoword  7327  unxpdomlem3  8028  fiming  8264  fiinfg  8265  sornom  8959  fin1a2s  9096  mulsub  10324  leltadd  10363  ltord1  10405  leord1  10406  eqord1  10407  divmul24  10580  expcan  12732  ltexp2  12733  fsum  14246  fprod  14458  isprm5  15205  ramub  15503  setcinv  16511  grpidpropd  17032  gsumpropd2lem  17044  cmnpropd  17973  unitpropd  18468  lidl1el  18987  gsumcom3  19971  1marepvmarrepid  20147  1marepvsma1  20155  ordtrest2  20765  filuni  21446  haustsms2  21697  blcomps  21955  blcom  21956  metnrmlem3  22419  cnmpt2pc  22482  icoopnst  22493  icccvx  22504  equivcfil  22849  volcn  23124  dvmptfsum  23486  cxple  24185  cxple3  24191  lnosub  26791  chirredlem2  28427  bhmafibid2  28769  metider  29058  ordtrest2NEW  29090  finxpreclem2  32186  fin2so  32349  cover2  32461  filbcmb  32488  isdrngo2  32710  crngohomfo  32758  unichnidl  32783  cdleme50eq  34630  dvhvaddcomN  35186  ismrc  36065  uhgr2edg  40416
  Copyright terms: Public domain W3C validator