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

Theorem 3coml 1124
Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3coml ((𝜓𝜒𝜑) → 𝜃)

Proof of Theorem 3coml
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213com23 1123 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1121 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  spc3egv  3587  omwordri  8593  oeword  8611  f1oen2g  8989  f1dom2g  8990  f1dom2gOLD  8991  f1imaenfi  9226  ordiso  9546  en3lplem2  9643  axdc3lem4  10483  ltasr  11130  adddir  11242  axltadd  11324  pnpcan2  11537  subdir  11685  ltaddsub  11725  leaddsub  11727  mulcan2g  11905  div13  11931  ltdiv2  12138  lediv2  12142  zdiv  12670  xadddir  13315  xadddi2r  13317  fzen  13558  fzrevral2  13627  fzshftral  13629  ssfzoulel  13766  fzind2  13791  flflp1  13813  mulbinom2  14226  digit1  14240  faclbnd5  14298  ccatlcan  14709  elicc4abs  15307  dvdsnegb  16259  muldvds1  16266  muldvds2  16267  dvdscmul  16268  dvdsmulc  16269  dvdscmulr  16270  dvdsmulcr  16271  dvdsgcd  16528  mulgcdr  16534  lcmgcdeq  16591  congr  16643  mulgnnass  19077  gaass  19265  elfm3  23903  mettri  24307  cnmet  24737  addcnlem  24829  bcthlem5  25305  isppw2  27097  vmappw  27098  bcmono  27260  sletr  27742  sltadd1im  27953  colinearalg  28798  ax5seglem1  28816  ax5seglem2  28817  vcdir  30453  vcass  30454  imsmetlem  30577  hvaddcan2  30958  hvsubcan2  30962  dfgcd3  36936  isbasisrelowllem1  36967  ltflcei  37214  fzmul  37347  brcnvrabga  37946  pclfinclN  39555  rabrenfdioph  42378  uun123p2  44393  isosctrlem1ALT  44517
  Copyright terms: Public domain W3C validator