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  8473  oaword1  8477  nnacan  8554  nnaword1  8555  elmapg  8774  fisseneq  9161  ltapr  10954  subadd  11381  ltaddsub  11609  leaddsub  11611  iooshf  13340  faclbnd4  14218  relexpsucl  14952  relexpsucr  14953  dvdsmulc  16208  lcmdvdsb  16538  infpnlem1  16836  fmf  23887  frgr3v  30299  nvs  30687  dipdi  30867  dipsubdi  30873  spansncol  31592  chirredlem2  32415  mdsymlem3  32429  isbasisrelowllem2  37500  ltflcei  37748  iscringd  38138  resubadd  42576  iunrelexp0  43885  uun123p4  44994  isosctrlem1ALT  45116  stoweidlem17  46203