Theorem 3comr 1125

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) Theorems shortened and reordered. (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 1123	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3com13 1124	1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3com23  1126  sbciegft  3802  oacan  8560  omlimcl  8590  nnacan  8640  dif1en  9174  dif1enOLD  9176  unfi  9185  en3lplem2  9627  le2tri3i  11365  ltaddsublt  11864  div12  11918  lemul12b  12098  zdivadd  12664  zdivmul  12665  elfz  13530  fzmmmeqm  13574  fzrev  13604  modmulnn  13906  digit2  14254  digit1  14255  faclbnd5  14316  hashfundm  14460  absdiflt  15336  absdifle  15337  dvds0lem  16286  dvdsmulc  16303  dvds2add  16309  dvds2sub  16310  dvdstr  16313  lcmdvds  16627  pospropd  18337  fmfil  23882  elfm  23885  psmettri2  24248  xmettri2  24279  stdbdmetval  24453  nmf2  24532  isclmi0  25049  iscvsi  25080  brbtwn  28878  colinearalglem3  28887  colinearalg  28889  isvciOLD  30561  nvtri  30651  nmooge0  30748  his7  31071  his2sub2  31074  braadd  31926  bramul  31927  cnlnadjlem2  32049  pjimai  32157  atcvati  32367  mdsymlem5  32388  bnj240  34730  bnj1189  35040  cusgredgex  35144  colineardim1  36079  ftc1anclem6  37722  brcnvrabga  38360  oaord3  43316  omord2com  43326  uun123p3  44835  stoweidlem2  46031  sigarperm  46889  leaddsuble  47326