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

Theorem 3comr 1119
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 1117 . 2 ((𝜓𝜑𝜒) → 𝜃)
323com13 1118 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  3com23  1120  oacan  7789  omlimcl  7819  nnacan  7869  en3lplem2  8673  le2tri3i  10351  ltaddsublt  10838  div12  10891  lemul12b  11064  zdivadd  11632  zdivmul  11633  elfz  12517  fzmmmeqm  12559  fzrev  12588  modmulnn  12874  digit2  13183  digit1  13184  faclbnd5  13271  swrdccatin2  13679  absdiflt  14248  absdifle  14249  dvds0lem  15186  dvdsmulc  15203  dvds2add  15209  dvds2sub  15210  dvdstr  15212  lcmdvds  15515  pospropd  17327  fmfil  21941  elfm  21944  psmettri2  22307  xmettri2  22338  stdbdmetval  22512  nmf2  22590  isclmi0  23090  iscvsi  23121  brbtwn  25970  colinearalglem3  25979  colinearalg  25981  isvciOLD  27736  nvtri  27826  nmooge0  27923  his7  28248  his2sub2  28251  braadd  29105  bramul  29106  cnlnadjlem2  29228  pjimai  29336  atcvati  29546  mdsymlem5  29567  bnj240  31066  bnj1189  31376  colineardim1  32466  ftc1anclem6  33795  uun123p3  39532  stoweidlem2  40714  sigarperm  41547  leaddsuble  41813
  Copyright terms: Public domain W3C validator