Theorem 3comr 1123

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

Syntax hints:   → wi 4   ∧ w3a 1085

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

This theorem is referenced by:  3com23  1124  oacan  8341  omlimcl  8371  nnacan  8421  dif1en  8907  unfi  8917  en3lplem2  9301  le2tri3i  11035  ltaddsublt  11532  div12  11585  lemul12b  11762  zdivadd  12321  zdivmul  12322  elfz  13174  fzmmmeqm  13218  fzrev  13248  modmulnn  13537  digit2  13879  digit1  13880  faclbnd5  13940  absdiflt  14957  absdifle  14958  dvds0lem  15904  dvdsmulc  15921  dvds2add  15927  dvds2sub  15928  dvdstr  15931  lcmdvds  16241  pospropd  17960  fmfil  23003  elfm  23006  psmettri2  23370  xmettri2  23401  stdbdmetval  23576  nmf2  23655  isclmi0  24167  iscvsi  24198  brbtwn  27170  colinearalglem3  27179  colinearalg  27181  isvciOLD  28843  nvtri  28933  nmooge0  29030  his7  29353  his2sub2  29356  braadd  30208  bramul  30209  cnlnadjlem2  30331  pjimai  30439  atcvati  30649  mdsymlem5  30670  bnj240  32578  bnj1189  32889  hashfundm  32974  cusgredgex  32983  colineardim1  34290  ftc1anclem6  35782  brcnvrabga  36404  uun123p3  42320  stoweidlem2  43433  sigarperm  44263  leaddsuble  44677