Theorem 3com13 1121

Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com13	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem 3com13

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1116	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp31 1109	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3comr  1122  3coml  1124  oacan  8570  oaword1  8574  nnacan  8650  nnaword1  8651  elmapg  8860  fisseneq  9284  ltapr  11079  subadd  11504  ltaddsub  11729  leaddsub  11731  iooshf  13451  faclbnd4  14309  relexpsucl  15031  relexpsucr  15032  dvdsmulc  16281  lcmdvdsb  16609  infpnlem1  16907  fmf  23937  frgr3v  30205  nvs  30593  dipdi  30773  dipsubdi  30779  spansncol  31498  chirredlem2  32321  mdsymlem3  32335  isbasisrelowllem2  37076  ltflcei  37322  iscringd  37712  resubadd  42090  iunrelexp0  43406  uun123p4  44525  isosctrlem1ALT  44647  stoweidlem17  45674