Theorem 3comr 1143

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3com23  1144  sbciegft  3776  oacan  8549  omlimcl  8579  nnacan  8630  dif1en  9170  unfi  9179  en3lplem2  9607  le2tri3i  11433  ltaddsublt  11936  div12  11989  lemul12b  12167  zdivadd  12763  zdivmul  12764  elfz  13638  fzmmmeqm  13684  fzrev  13714  modmulnn  14022  digit2  14373  digit1  14374  faclbnd5  14435  hashfundm  14580  absdiflt  15478  absdifle  15479  dvds0lem  16429  dvdsmulc  16446  dvds2add  16453  dvds2sub  16454  dvdstr  16457  lcmdvds  16776  pospropd  18492  fmfil  24256  elfm  24259  psmettri2  24621  xmettri2  24652  stdbdmetval  24826  nmf2  24905  isclmi0  25412  iscvsi  25443  brbtwn  29470  colinearalglem3  29479  colinearalg  29481  isvciOLD  31175  nvtri  31265  nmooge0  31362  his7  31685  his2sub2  31688  braadd  32540  bramul  32541  cnlnadjlem2  32663  pjimai  32771  atcvati  32981  mdsymlem5  33002  bnj240  35323  bnj1189  35632  cusgredgex  35885  colineardim1  36806  ftc1anclem6  38596  brcnvrabga  39254  oaord3  44278  omord2com  44288  uun123p3  45778  stoweidlem2  46981  sigarperm  47839  leaddsuble  48336