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

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

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213com12 1124 . 2 ((𝜓𝜑𝜒) → 𝜃)
323com13 1125 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3com23  1127  oacan  8496  omlimcl  8526  nnacan  8576  dif1en  9107  dif1enOLD  9109  unfi  9119  en3lplem2  9554  le2tri3i  11290  ltaddsublt  11787  div12  11840  lemul12b  12017  zdivadd  12579  zdivmul  12580  elfz  13436  fzmmmeqm  13480  fzrev  13510  modmulnn  13800  digit2  14145  digit1  14146  faclbnd5  14204  absdiflt  15208  absdifle  15209  dvds0lem  16154  dvdsmulc  16171  dvds2add  16177  dvds2sub  16178  dvdstr  16181  lcmdvds  16489  pospropd  18221  fmfil  23311  elfm  23314  psmettri2  23678  xmettri2  23709  stdbdmetval  23886  nmf2  23965  isclmi0  24477  iscvsi  24508  brbtwn  27890  colinearalglem3  27899  colinearalg  27901  isvciOLD  29564  nvtri  29654  nmooge0  29751  his7  30074  his2sub2  30077  braadd  30929  bramul  30930  cnlnadjlem2  31052  pjimai  31160  atcvati  31370  mdsymlem5  31391  bnj240  33368  bnj1189  33678  hashfundm  33763  cusgredgex  33772  colineardim1  34692  ftc1anclem6  36202  brcnvrabga  36849  oaord3  41670  omord2com  41680  uun123p3  43181  stoweidlem2  44329  sigarperm  45187  leaddsuble  45615
  Copyright terms: Public domain W3C validator