Theorem 3com13 1125

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 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp31 1112	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3comr  1126  3coml  1128  oacan  8586  oaword1  8590  nnacan  8666  nnaword1  8667  elmapg  8879  fisseneq  9293  ltapr  11085  subadd  11511  ltaddsub  11737  leaddsub  11739  iooshf  13466  faclbnd4  14336  relexpsucl  15070  relexpsucr  15071  dvdsmulc  16321  lcmdvdsb  16650  infpnlem1  16948  fmf  23953  frgr3v  30294  nvs  30682  dipdi  30862  dipsubdi  30868  spansncol  31587  chirredlem2  32410  mdsymlem3  32424  isbasisrelowllem2  37357  ltflcei  37615  iscringd  38005  resubadd  42409  iunrelexp0  43715  uun123p4  44832  isosctrlem1ALT  44954  stoweidlem17  46032