Theorem 3comr 1125

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3com23  1126  sbciegft  3773  oacan  8458  omlimcl  8488  nnacan  8538  dif1en  9066  unfi  9075  en3lplem2  9498  le2tri3i  11238  ltaddsublt  11739  div12  11793  lemul12b  11973  zdivadd  12539  zdivmul  12540  elfz  13408  fzmmmeqm  13452  fzrev  13482  modmulnn  13788  digit2  14138  digit1  14139  faclbnd5  14200  hashfundm  14344  absdiflt  15220  absdifle  15221  dvds0lem  16172  dvdsmulc  16189  dvds2add  16196  dvds2sub  16197  dvdstr  16200  lcmdvds  16514  pospropd  18226  fmfil  23854  elfm  23857  psmettri2  24219  xmettri2  24250  stdbdmetval  24424  nmf2  24503  isclmi0  25020  iscvsi  25051  brbtwn  28872  colinearalglem3  28881  colinearalg  28883  isvciOLD  30552  nvtri  30642  nmooge0  30739  his7  31062  his2sub2  31065  braadd  31917  bramul  31918  cnlnadjlem2  32040  pjimai  32148  atcvati  32358  mdsymlem5  32379  bnj240  34703  bnj1189  35013  cusgredgex  35158  colineardim1  36095  ftc1anclem6  37738  brcnvrabga  38370  oaord3  43325  omord2com  43335  uun123p3  44843  stoweidlem2  46040  sigarperm  46898  leaddsuble  47328