Theorem 3com13 1124

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3comr  1125  3coml  1127  oacan  8515  oaword1  8519  nnacan  8595  nnaword1  8596  elmapg  8815  fisseneq  9211  ltapr  11005  subadd  11431  ltaddsub  11659  leaddsub  11661  iooshf  13394  faclbnd4  14269  relexpsucl  15004  relexpsucr  15005  dvdsmulc  16260  lcmdvdsb  16590  infpnlem1  16888  fmf  23839  frgr3v  30211  nvs  30599  dipdi  30779  dipsubdi  30785  spansncol  31504  chirredlem2  32327  mdsymlem3  32341  isbasisrelowllem2  37351  ltflcei  37609  iscringd  37999  resubadd  42374  iunrelexp0  43698  uun123p4  44808  isosctrlem1ALT  44930  stoweidlem17  46022