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

Theorem 3coml 1128
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 1127 . 2 ((𝜑𝜒𝜓) → 𝜃)
323com13 1125 1 ((𝜓𝜒𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  spc3egv  3603  omwordri  8610  oeword  8628  f1oen2g  9009  f1dom2g  9010  f1imaenfi  9235  ordiso  9556  en3lplem2  9653  axdc3lem4  10493  ltasr  11140  adddir  11252  axltadd  11334  pnpcan2  11549  subdir  11697  ltaddsub  11737  leaddsub  11739  mulcan2g  11917  div13  11943  ltdiv2  12154  lediv2  12158  zdiv  12688  xadddir  13338  xadddi2r  13340  fzen  13581  fzrevral2  13653  fzshftral  13655  ssfzoulel  13799  fzind2  13824  flflp1  13847  mulbinom2  14262  digit1  14276  faclbnd5  14337  ccatlcan  14756  elicc4abs  15358  dvdsnegb  16311  muldvds1  16318  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  dvdscmulr  16322  dvdsmulcr  16323  dvdsgcd  16581  mulgcdr  16587  lcmgcdeq  16649  congr  16701  mulgnnass  19127  gaass  19315  elfm3  23958  mettri  24362  cnmet  24792  addcnlem  24886  bcthlem5  25362  isppw2  27158  vmappw  27159  bcmono  27321  sletr  27803  sltadd1im  28018  colinearalg  28925  ax5seglem1  28943  ax5seglem2  28944  vcdir  30585  vcass  30586  imsmetlem  30709  hvaddcan2  31090  hvsubcan2  31094  dfgcd3  37325  isbasisrelowllem1  37356  ltflcei  37615  fzmul  37748  brcnvrabga  38343  pclfinclN  39952  rabrenfdioph  42825  uun123p2  44830  isosctrlem1ALT  44954
  Copyright terms: Public domain W3C validator