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 210  df-an 400  df-3an 1086
This theorem is referenced by:  spc3egv  3590  omwordri  8188  oeword  8206  f1oen2g  8516  f1dom2g  8517  ordiso  8971  en3lplem2  9067  axdc3lem4  9867  ltasr  10514  adddir  10624  axltadd  10706  pnpcan2  10918  subdir  11066  ltaddsub  11106  leaddsub  11108  mulcan2g  11286  div13  11311  ltdiv2  11518  lediv2  11522  zdiv  12045  xadddir  12682  xadddi2r  12684  fzen  12924  fzrevral2  12993  fzshftral  12995  ssfzoulel  13131  fzind2  13155  flflp1  13177  mulbinom2  13585  digit1  13599  faclbnd5  13659  ccatlcan  14076  relexpreld  14395  elicc4abs  14675  dvdsnegb  15623  muldvds1  15630  muldvds2  15631  dvdscmul  15632  dvdsmulc  15633  dvdscmulr  15634  dvdsmulcr  15635  dvdsgcd  15886  mulgcdr  15892  lcmgcdeq  15950  congr  16002  mulgnnass  18258  gaass  18423  elfm3  22551  mettri  22955  cnmet  23373  addcnlem  23465  bcthlem5  23928  isppw2  25696  vmappw  25697  bcmono  25857  colinearalg  26700  ax5seglem1  26718  ax5seglem2  26719  vcdir  28345  vcass  28346  imsmetlem  28469  hvaddcan2  28850  hvsubcan2  28854  sletr  33262  dfgcd3  34651  isbasisrelowllem1  34684  ltflcei  34955  fzmul  35089  brcnvrabga  35669  pclfinclN  37156  rabrenfdioph  39608  uun123p2  41373  isosctrlem1ALT  41497
  Copyright terms: Public domain W3C validator