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

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

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  8157  omlimcl  8187  nnacan  8237  en3lplem2  9060  le2tri3i  10759  ltaddsublt  11256  div12  11309  lemul12b  11486  zdivadd  12041  zdivmul  12042  elfz  12891  fzmmmeqm  12935  fzrev  12965  modmulnn  13252  digit2  13593  digit1  13594  faclbnd5  13654  absdiflt  14669  absdifle  14670  dvds0lem  15612  dvdsmulc  15629  dvds2add  15635  dvds2sub  15636  dvdstr  15638  lcmdvds  15942  pospropd  17736  fmfil  22549  elfm  22552  psmettri2  22916  xmettri2  22947  stdbdmetval  23121  nmf2  23199  isclmi0  23703  iscvsi  23734  brbtwn  26693  colinearalglem3  26702  colinearalg  26704  isvciOLD  28363  nvtri  28453  nmooge0  28550  his7  28873  his2sub2  28876  braadd  29728  bramul  29729  cnlnadjlem2  29851  pjimai  29959  atcvati  30169  mdsymlem5  30190  bnj240  32079  bnj1189  32391  hashfundm  32464  cusgredgex  32481  colineardim1  33635  ftc1anclem6  35135  brcnvrabga  35759  uun123p3  41517  stoweidlem2  42644  sigarperm  43474  leaddsuble  43854