Theorem 3comr 1120

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

Syntax hints:   → wi 4   ∧ w3a 1082

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 1084

This theorem is referenced by:  3com23  1121  oacan  8167  omlimcl  8197  nnacan  8247  en3lplem2  9069  le2tri3i  10763  ltaddsublt  11260  div12  11313  lemul12b  11490  zdivadd  12047  zdivmul  12048  elfz  12895  fzmmmeqm  12937  fzrev  12967  modmulnn  13254  digit2  13594  digit1  13595  faclbnd5  13655  absdiflt  14672  absdifle  14673  dvds0lem  15615  dvdsmulc  15632  dvds2add  15638  dvds2sub  15639  dvdstr  15641  lcmdvds  15947  pospropd  17739  fmfil  22547  elfm  22550  psmettri2  22914  xmettri2  22945  stdbdmetval  23119  nmf2  23197  isclmi0  23697  iscvsi  23728  brbtwn  26683  colinearalglem3  26692  colinearalg  26694  isvciOLD  28355  nvtri  28445  nmooge0  28542  his7  28865  his2sub2  28868  braadd  29720  bramul  29721  cnlnadjlem2  29843  pjimai  29951  atcvati  30161  mdsymlem5  30182  bnj240  31990  bnj1189  32302  hashfundm  32375  cusgredgex  32389  colineardim1  33543  ftc1anclem6  35005  brcnvrabga  35632  uun123p3  41219  stoweidlem2  42361  sigarperm  43191  leaddsuble  43571