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

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

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213coml 1263 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1263 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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  df-3an 1032
This theorem is referenced by:  oacan  7489  omlimcl  7519  nnacan  7569  en3lplem2  8369  le2tri3i  10015  ltaddsublt  10500  div12  10553  lemul12b  10726  zdivadd  11277  zdivmul  11278  elfz  12155  fzmmmeqm  12197  fzrev  12225  modmulnn  12502  digit2  12811  digit1  12812  faclbnd5  12899  swrdccatin2  13281  absdiflt  13848  absdifle  13849  dvds0lem  14773  dvdsmulc  14790  dvds2add  14796  dvds2sub  14797  dvdstr  14799  mulmoddvds  14832  lcmdvds  15102  pospropd  16900  fmfil  21497  elfm  21500  psmettri2  21863  xmettri2  21893  stdbdmetval  22067  nmf2  22145  isclmi0  22634  iscvsi  22663  brbtwn  25494  colinearalglem3  25503  colinearalg  25505  isvciOLD  26600  nvtri  26700  nmooge0  26809  his7  27134  his2sub2  27137  braadd  27991  bramul  27992  cnlnadjlem2  28114  pjimai  28222  atcvati  28432  mdsymlem5  28453  bnj240  29821  bnj1189  30134  colineardim1  31141  ftc1anclem6  32460  uun123p3  37859  stoweidlem2  38696  sigarperm  39499  leaddsuble  40167
  Copyright terms: Public domain W3C validator