Theorem 3comr 1126

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 1124	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3com13 1125	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  1127  sbciegft  3766  oacan  8474  omlimcl  8504  nnacan  8555  dif1en  9087  unfi  9096  en3lplem2  9523  le2tri3i  11264  ltaddsublt  11765  div12  11819  lemul12b  11999  zdivadd  12564  zdivmul  12565  elfz  13430  fzmmmeqm  13474  fzrev  13504  modmulnn  13810  digit2  14160  digit1  14161  faclbnd5  14222  hashfundm  14366  absdiflt  15242  absdifle  15243  dvds0lem  16194  dvdsmulc  16211  dvds2add  16218  dvds2sub  16219  dvdstr  16222  lcmdvds  16536  pospropd  18249  fmfil  23887  elfm  23890  psmettri2  24252  xmettri2  24283  stdbdmetval  24457  nmf2  24536  isclmi0  25043  iscvsi  25074  brbtwn  28956  colinearalglem3  28965  colinearalg  28967  isvciOLD  30640  nvtri  30730  nmooge0  30827  his7  31150  his2sub2  31153  braadd  32005  bramul  32006  cnlnadjlem2  32128  pjimai  32236  atcvati  32446  mdsymlem5  32467  bnj240  34848  bnj1189  35157  cusgredgex  35310  colineardim1  36249  ftc1anclem6  38010  brcnvrabga  38654  oaord3  43723  omord2com  43733  uun123p3  45240  stoweidlem2  46434  sigarperm  47292  leaddsuble  47731