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

Theorem 3comr 1122
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 1120 . 2 ((𝜓𝜑𝜒) → 𝜃)
323com13 1121 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3com23  1123  oacan  8170  omlimcl  8200  nnacan  8250  en3lplem2  9073  le2tri3i  10768  ltaddsublt  11265  div12  11318  lemul12b  11495  zdivadd  12050  zdivmul  12051  elfz  12900  fzmmmeqm  12944  fzrev  12974  modmulnn  13261  digit2  13602  digit1  13603  faclbnd5  13663  absdiflt  14677  absdifle  14678  dvds0lem  15620  dvdsmulc  15637  dvds2add  15643  dvds2sub  15644  dvdstr  15646  lcmdvds  15950  pospropd  17744  fmfil  22552  elfm  22555  psmettri2  22919  xmettri2  22950  stdbdmetval  23124  nmf2  23202  isclmi0  23706  iscvsi  23737  brbtwn  26696  colinearalglem3  26705  colinearalg  26707  isvciOLD  28366  nvtri  28456  nmooge0  28553  his7  28876  his2sub2  28879  braadd  29731  bramul  29732  cnlnadjlem2  29854  pjimai  29962  atcvati  30172  mdsymlem5  30193  bnj240  32026  bnj1189  32338  hashfundm  32411  cusgredgex  32425  colineardim1  33579  ftc1anclem6  35080  brcnvrabga  35704  uun123p3  41437  stoweidlem2  42570  sigarperm  43400  leaddsuble  43780
  Copyright terms: Public domain W3C validator