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  3777  oacan  8475  omlimcl  8505  nnacan  8556  dif1en  9086  unfi  9095  en3lplem2  9522  le2tri3i  11263  ltaddsublt  11764  div12  11818  lemul12b  11998  zdivadd  12563  zdivmul  12564  elfz  13429  fzmmmeqm  13473  fzrev  13503  modmulnn  13809  digit2  14159  digit1  14160  faclbnd5  14221  hashfundm  14365  absdiflt  15241  absdifle  15242  dvds0lem  16193  dvdsmulc  16210  dvds2add  16217  dvds2sub  16218  dvdstr  16221  lcmdvds  16535  pospropd  18248  fmfil  23888  elfm  23891  psmettri2  24253  xmettri2  24284  stdbdmetval  24458  nmf2  24537  isclmi0  25054  iscvsi  25085  brbtwn  28972  colinearalglem3  28981  colinearalg  28983  isvciOLD  30655  nvtri  30745  nmooge0  30842  his7  31165  his2sub2  31168  braadd  32020  bramul  32021  cnlnadjlem2  32143  pjimai  32251  atcvati  32461  mdsymlem5  32482  bnj240  34855  bnj1189  35165  cusgredgex  35316  colineardim1  36255  ftc1anclem6  37899  brcnvrabga  38535  oaord3  43534  omord2com  43544  uun123p3  45051  stoweidlem2  46246  sigarperm  47104  leaddsuble  47543