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  3779  oacan  8592  omlimcl  8622  nnacan  8673  dif1en  9213  unfi  9222  en3lplem2  9649  le2tri3i  11477  ltaddsublt  11981  div12  12034  lemul12b  12212  zdivadd  12808  zdivmul  12809  elfz  13683  fzmmmeqm  13729  fzrev  13759  modmulnn  14067  digit2  14419  digit1  14420  faclbnd5  14481  hashfundm  14626  absdiflt  15526  absdifle  15527  dvds0lem  16477  dvdsmulc  16494  dvds2add  16501  dvds2sub  16502  dvdstr  16505  lcmdvds  16824  pospropd  18540  fmfil  24307  elfm  24310  psmettri2  24672  xmettri2  24703  stdbdmetval  24877  nmf2  24956  isclmi0  25463  iscvsi  25494  brbtwn  29523  colinearalglem3  29532  colinearalg  29534  isvciOLD  31228  nvtri  31318  nmooge0  31415  his7  31738  his2sub2  31741  braadd  32593  bramul  32594  cnlnadjlem2  32716  pjimai  32824  atcvati  33034  mdsymlem5  33055  bnj240  35434  bnj1189  35743  cusgredgex  36097  elpssmo  36666  colineardim1  37034  ftc1anclem6  38877  brcnvrabga  39533  oaord3  44549  omord2com  44559  uun123p3  46047  stoweidlem2  47279  sigarperm  48137  leaddsuble  48634