Theorem 3comr 1125

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 1123	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3com13 1124	1 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3com23  1126  oacan  8547  omlimcl  8577  nnacan  8627  dif1en  9159  dif1enOLD  9161  unfi  9171  en3lplem2  9607  le2tri3i  11343  ltaddsublt  11840  div12  11893  lemul12b  12070  zdivadd  12632  zdivmul  12633  elfz  13489  fzmmmeqm  13533  fzrev  13563  modmulnn  13853  digit2  14198  digit1  14199  faclbnd5  14257  hashfundm  14401  absdiflt  15263  absdifle  15264  dvds0lem  16209  dvdsmulc  16226  dvds2add  16232  dvds2sub  16233  dvdstr  16236  lcmdvds  16544  pospropd  18279  fmfil  23447  elfm  23450  psmettri2  23814  xmettri2  23845  stdbdmetval  24022  nmf2  24101  isclmi0  24613  iscvsi  24644  brbtwn  28154  colinearalglem3  28163  colinearalg  28165  isvciOLD  29828  nvtri  29918  nmooge0  30015  his7  30338  his2sub2  30341  braadd  31193  bramul  31194  cnlnadjlem2  31316  pjimai  31424  atcvati  31634  mdsymlem5  31655  bnj240  33705  bnj1189  34015  cusgredgex  34107  colineardim1  35028  ftc1anclem6  36561  brcnvrabga  37206  oaord3  42032  omord2com  42042  uun123p3  43562  stoweidlem2  44708  sigarperm  45566  leaddsuble  45995