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

Theorem 3comr 1271
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 1270 . 2 ((𝜓𝜒𝜑) → 𝜃)
323coml 1270 1 ((𝜒𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  oacan  7613  omlimcl  7643  nnacan  7693  en3lplem2  8497  le2tri3i  10152  ltaddsublt  10639  div12  10692  lemul12b  10865  zdivadd  11433  zdivmul  11434  elfz  12317  fzmmmeqm  12359  fzrev  12388  modmulnn  12671  digit2  12980  digit1  12981  faclbnd5  13068  swrdccatin2  13468  absdiflt  14038  absdifle  14039  dvds0lem  14973  dvdsmulc  14990  dvds2add  14996  dvds2sub  14997  dvdstr  14999  mulmoddvds  15032  lcmdvds  15302  pospropd  17115  fmfil  21729  elfm  21732  psmettri2  22095  xmettri2  22126  stdbdmetval  22300  nmf2  22378  isclmi0  22879  iscvsi  22910  brbtwn  25760  colinearalglem3  25769  colinearalg  25771  isvciOLD  27405  nvtri  27495  nmooge0  27592  his7  27917  his2sub2  27920  braadd  28774  bramul  28775  cnlnadjlem2  28897  pjimai  29005  atcvati  29215  mdsymlem5  29236  bnj240  30739  bnj1189  31051  colineardim1  32143  ftc1anclem6  33461  uun123p3  38858  stoweidlem2  39982  sigarperm  40812  leaddsuble  41074
  Copyright terms: Public domain W3C validator