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  3774  oacan  8472  omlimcl  8502  nnacan  8552  dif1en  9082  unfi  9091  en3lplem2  9514  le2tri3i  11254  ltaddsublt  11755  div12  11809  lemul12b  11989  zdivadd  12554  zdivmul  12555  elfz  13420  fzmmmeqm  13464  fzrev  13494  modmulnn  13800  digit2  14150  digit1  14151  faclbnd5  14212  hashfundm  14356  absdiflt  15232  absdifle  15233  dvds0lem  16184  dvdsmulc  16201  dvds2add  16208  dvds2sub  16209  dvdstr  16212  lcmdvds  16526  pospropd  18239  fmfil  23879  elfm  23882  psmettri2  24244  xmettri2  24275  stdbdmetval  24449  nmf2  24528  isclmi0  25045  iscvsi  25076  brbtwn  28898  colinearalglem3  28907  colinearalg  28909  isvciOLD  30581  nvtri  30671  nmooge0  30768  his7  31091  his2sub2  31094  braadd  31946  bramul  31947  cnlnadjlem2  32069  pjimai  32177  atcvati  32387  mdsymlem5  32408  bnj240  34783  bnj1189  35093  cusgredgex  35238  colineardim1  36177  ftc1anclem6  37811  brcnvrabga  38447  oaord3  43449  omord2com  43459  uun123p3  44967  stoweidlem2  46162  sigarperm  47020  leaddsuble  47459