Theorem 3com13 1130

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3comr  1131  3coml  1133  oacan  8473  oaword1  8477  nnacan  8554  nnaword1  8555  elmapg  8776  fisseneq  9163  ltapr  10959  subadd  11387  ltaddsub  11615  leaddsub  11617  iooshf  13370  faclbnd4  14250  relexpsucl  14984  relexpsucr  14985  dvdsmulc  16243  lcmdvdsb  16573  infpnlem1  16872  fmf  23928  frgr3v  30363  nvs  30752  dipdi  30932  dipsubdi  30938  spansncol  31657  chirredlem2  32480  mdsymlem3  32494  isbasisrelowllem2  37718  ltflcei  37975  iscringd  38365  resubadd  42856  iunrelexp0  44146  uun123p4  45255  isosctrlem1ALT  45377  stoweidlem17  46460