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  8489  oaword1  8493  nnacan  8569  nnaword1  8570  elmapg  8789  fisseneq  9180  ltapr  10974  subadd  11400  ltaddsub  11628  leaddsub  11630  iooshf  13363  faclbnd4  14238  relexpsucl  14973  relexpsucr  14974  dvdsmulc  16229  lcmdvdsb  16559  infpnlem1  16857  fmf  23865  frgr3v  30254  nvs  30642  dipdi  30822  dipsubdi  30828  spansncol  31547  chirredlem2  32370  mdsymlem3  32384  isbasisrelowllem2  37337  ltflcei  37595  iscringd  37985  resubadd  42360  iunrelexp0  43684  uun123p4  44794  isosctrlem1ALT  44916  stoweidlem17  46008