Theorem 3comr 1116

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

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com12 1114	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3com13 1115	1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3com23  1117  oacan  7912  omlimcl  7942  nnacan  7992  en3lplem2  8805  le2tri3i  10506  ltaddsublt  11002  div12  11055  lemul12b  11234  zdivadd  11800  zdivmul  11801  elfz  12649  fzmmmeqm  12691  fzrev  12721  modmulnn  13007  digit2  13316  digit1  13317  faclbnd5  13403  swrdccatin2  13856  absdiflt  14464  absdifle  14465  dvds0lem  15399  dvdsmulc  15416  dvds2add  15422  dvds2sub  15423  dvdstr  15425  lcmdvds  15727  pospropd  17520  fmfil  22156  elfm  22159  psmettri2  22522  xmettri2  22553  stdbdmetval  22727  nmf2  22805  isclmi0  23305  iscvsi  23336  brbtwn  26248  colinearalglem3  26257  colinearalg  26259  isvciOLD  28007  nvtri  28097  nmooge0  28194  his7  28519  his2sub2  28522  braadd  29376  bramul  29377  cnlnadjlem2  29499  pjimai  29607  atcvati  29817  mdsymlem5  29838  bnj240  31367  bnj1189  31676  colineardim1  32757  ftc1anclem6  34099  brcnvrabga  34722  uun123p3  39962  stoweidlem2  41128  sigarperm  41958  leaddsuble  42321