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  8477  oaword1  8481  nnacan  8558  nnaword1  8559  elmapg  8780  fisseneq  9167  ltapr  10962  subadd  11390  ltaddsub  11618  leaddsub  11620  iooshf  13373  faclbnd4  14253  relexpsucl  14987  relexpsucr  14988  dvdsmulc  16246  lcmdvdsb  16576  infpnlem1  16875  fmf  23923  frgr3v  30363  nvs  30752  dipdi  30932  dipsubdi  30938  spansncol  31657  chirredlem2  32480  mdsymlem3  32494  isbasisrelowllem2  37689  ltflcei  37946  iscringd  38336  resubadd  42828  iunrelexp0  44150  uun123p4  45259  isosctrlem1ALT  45381  stoweidlem17  46466