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

This theorem is referenced by:  3com23  1124  oacan  8552  omlimcl  8582  nnacan  8632  dif1en  9164  dif1enOLD  9166  unfi  9176  en3lplem2  9612  le2tri3i  11350  ltaddsublt  11847  div12  11900  lemul12b  12077  zdivadd  12639  zdivmul  12640  elfz  13496  fzmmmeqm  13540  fzrev  13570  modmulnn  13860  digit2  14205  digit1  14206  faclbnd5  14264  hashfundm  14408  absdiflt  15270  absdifle  15271  dvds0lem  16216  dvdsmulc  16233  dvds2add  16239  dvds2sub  16240  dvdstr  16243  lcmdvds  16551  pospropd  18286  fmfil  23670  elfm  23673  psmettri2  24037  xmettri2  24068  stdbdmetval  24245  nmf2  24324  isclmi0  24847  iscvsi  24878  brbtwn  28422  colinearalglem3  28431  colinearalg  28433  isvciOLD  30098  nvtri  30188  nmooge0  30285  his7  30608  his2sub2  30611  braadd  31463  bramul  31464  cnlnadjlem2  31586  pjimai  31694  atcvati  31904  mdsymlem5  31925  bnj240  34006  bnj1189  34316  cusgredgex  34408  colineardim1  35335  ftc1anclem6  36871  brcnvrabga  37516  oaord3  42346  omord2com  42356  uun123p3  43876  stoweidlem2  45018  sigarperm  45876  leaddsuble  46305