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

This theorem is referenced by:  3com23  1126  sbciegft  3842  oacan  8604  omlimcl  8634  nnacan  8684  dif1en  9226  dif1enOLD  9228  unfi  9238  en3lplem2  9682  le2tri3i  11420  ltaddsublt  11917  div12  11971  lemul12b  12151  zdivadd  12714  zdivmul  12715  elfz  13573  fzmmmeqm  13617  fzrev  13647  modmulnn  13940  digit2  14285  digit1  14286  faclbnd5  14347  hashfundm  14491  absdiflt  15366  absdifle  15367  dvds0lem  16315  dvdsmulc  16332  dvds2add  16338  dvds2sub  16339  dvdstr  16342  lcmdvds  16655  pospropd  18397  fmfil  23973  elfm  23976  psmettri2  24340  xmettri2  24371  stdbdmetval  24548  nmf2  24627  isclmi0  25150  iscvsi  25181  brbtwn  28932  colinearalglem3  28941  colinearalg  28943  isvciOLD  30612  nvtri  30702  nmooge0  30799  his7  31122  his2sub2  31125  braadd  31977  bramul  31978  cnlnadjlem2  32100  pjimai  32208  atcvati  32418  mdsymlem5  32439  bnj240  34675  bnj1189  34985  cusgredgex  35089  colineardim1  36025  ftc1anclem6  37658  brcnvrabga  38298  oaord3  43254  omord2com  43264  uun123p3  44782  stoweidlem2  45923  sigarperm  46781  leaddsuble  47212