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

Theorem 3comr 1265
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 1264 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1264 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  oacan  7515  omlimcl  7545  nnacan  7595  en3lplem2  8395  le2tri3i  10046  ltaddsublt  10533  div12  10586  lemul12b  10759  zdivadd  11324  zdivmul  11325  elfz  12203  fzmmmeqm  12245  fzrev  12273  modmulnn  12550  digit2  12859  digit1  12860  faclbnd5  12947  swrdccatin2  13338  absdiflt  13905  absdifle  13906  dvds0lem  14830  dvdsmulc  14847  dvds2add  14853  dvds2sub  14854  dvdstr  14856  mulmoddvds  14889  lcmdvds  15159  pospropd  16957  fmfil  21558  elfm  21561  psmettri2  21924  xmettri2  21955  stdbdmetval  22129  nmf2  22207  isclmi0  22706  iscvsi  22737  brbtwn  25579  colinearalglem3  25588  colinearalg  25590  isvciOLD  26819  nvtri  26909  nmooge0  27006  his7  27331  his2sub2  27334  braadd  28188  bramul  28189  cnlnadjlem2  28311  pjimai  28419  atcvati  28629  mdsymlem5  28650  bnj240  30018  bnj1189  30331  colineardim1  31338  ftc1anclem6  32660  uun123p3  38059  stoweidlem2  38895  sigarperm  39698  leaddsuble  40343
  Copyright terms: Public domain W3C validator