Theorem 3comr 1121

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3com23  1122  oacan  8168  omlimcl  8198  nnacan  8248  en3lplem2  9070  le2tri3i  10764  ltaddsublt  11261  div12  11314  lemul12b  11491  zdivadd  12047  zdivmul  12048  elfz  12892  fzmmmeqm  12934  fzrev  12964  modmulnn  13251  digit2  13591  digit1  13592  faclbnd5  13652  absdiflt  14671  absdifle  14672  dvds0lem  15614  dvdsmulc  15631  dvds2add  15637  dvds2sub  15638  dvdstr  15640  lcmdvds  15946  pospropd  17738  fmfil  22546  elfm  22549  psmettri2  22913  xmettri2  22944  stdbdmetval  23118  nmf2  23196  isclmi0  23696  iscvsi  23727  brbtwn  26679  colinearalglem3  26688  colinearalg  26690  isvciOLD  28351  nvtri  28441  nmooge0  28538  his7  28861  his2sub2  28864  braadd  29716  bramul  29717  cnlnadjlem2  29839  pjimai  29947  atcvati  30157  mdsymlem5  30178  bnj240  31964  bnj1189  32276  hashfundm  32349  cusgredgex  32363  colineardim1  33517  ftc1anclem6  34966  brcnvrabga  35593  uun123p3  41138  stoweidlem2  42280  sigarperm  43110  leaddsuble  43490