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

Theorem 3comr 1125
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 1123 . 2 ((𝜓𝜑𝜒) → 𝜃)
323com13 1124 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 206  df-an 397  df-3an 1089
This theorem is referenced by:  3com23  1126  oacan  8491  omlimcl  8521  nnacan  8571  dif1en  9100  dif1enOLD  9102  unfi  9112  en3lplem2  9545  le2tri3i  11281  ltaddsublt  11778  div12  11831  lemul12b  12008  zdivadd  12570  zdivmul  12571  elfz  13422  fzmmmeqm  13466  fzrev  13496  modmulnn  13786  digit2  14131  digit1  14132  faclbnd5  14190  absdiflt  15194  absdifle  15195  dvds0lem  16141  dvdsmulc  16158  dvds2add  16164  dvds2sub  16165  dvdstr  16168  lcmdvds  16476  pospropd  18208  fmfil  23279  elfm  23282  psmettri2  23646  xmettri2  23677  stdbdmetval  23854  nmf2  23933  isclmi0  24445  iscvsi  24476  brbtwn  27734  colinearalglem3  27743  colinearalg  27745  isvciOLD  29408  nvtri  29498  nmooge0  29595  his7  29918  his2sub2  29921  braadd  30773  bramul  30774  cnlnadjlem2  30896  pjimai  31004  atcvati  31214  mdsymlem5  31235  bnj240  33180  bnj1189  33490  hashfundm  33575  cusgredgex  33584  colineardim1  34613  ftc1anclem6  36123  brcnvrabga  36770  oaord3  41565  omord2com  41574  uun123p3  43035  stoweidlem2  44175  sigarperm  45033  leaddsuble  45461
  Copyright terms: Public domain W3C validator