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  8475  oaword1  8479  nnacan  8556  nnaword1  8557  elmapg  8776  fisseneq  9163  ltapr  10956  subadd  11383  ltaddsub  11611  leaddsub  11613  iooshf  13342  faclbnd4  14220  relexpsucl  14954  relexpsucr  14955  dvdsmulc  16210  lcmdvdsb  16540  infpnlem1  16838  fmf  23889  frgr3v  30350  nvs  30738  dipdi  30918  dipsubdi  30924  spansncol  31643  chirredlem2  32466  mdsymlem3  32480  isbasisrelowllem2  37561  ltflcei  37809  iscringd  38199  resubadd  42634  iunrelexp0  43943  uun123p4  45052  isosctrlem1ALT  45174  stoweidlem17  46261