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 ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3com23  1144  sbciegft  3782  oacan  8534  omlimcl  8564  nnacan  8615  dif1en  9147  unfi  9156  en3lplem2  9583  le2tri3i  11341  ltaddsublt  11842  div12  11895  lemul12b  12073  zdivadd  12668  zdivmul  12669  elfz  13542  fzmmmeqm  13587  fzrev  13617  modmulnn  13924  digit2  14274  digit1  14275  faclbnd5  14336  hashfundm  14481  absdiflt  15371  absdifle  15372  dvds0lem  16325  dvdsmulc  16342  dvds2add  16349  dvds2sub  16350  dvdstr  16353  lcmdvds  16667  pospropd  18382  fmfil  24082  elfm  24085  psmettri2  24447  xmettri2  24478  stdbdmetval  24652  nmf2  24731  isclmi0  25238  iscvsi  25269  brbtwn  29230  colinearalglem3  29239  colinearalg  29241  isvciOLD  30913  nvtri  31003  nmooge0  31100  his7  31423  his2sub2  31426  braadd  32278  bramul  32279  cnlnadjlem2  32401  pjimai  32509  atcvati  32719  mdsymlem5  32740  bnj240  35069  bnj1189  35378  cusgredgex  35595  colineardim1  36534  ftc1anclem6  38330  brcnvrabga  38972  oaord3  44002  omord2com  44012  uun123p3  45502  stoweidlem2  46699  sigarperm  47557  leaddsuble  48017