Theorem 3com13 1142

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3coml  1145  oacan  8539  oaword1  8543  nnacan  8620  nnaword1  8621  elmapg  8842  fisseneq  9230  ltapr  11045  subadd  11475  ltaddsub  11703  leaddsub  11705  iooshf  13469  faclbnd4  14351  relexpsucl  15092  relexpsucr  15093  dvdsmulc  16363  lcmdvdsb  16693  infpnlem1  16992  fmf  24153  frgr3v  30697  nvs  31086  dipdi  31266  dipsubdi  31272  spansncol  31991  chirredlem2  32814  mdsymlem3  32828  isbasisrelowllem2  38059  ltflcei  38316  iscringd  38707  resubadd  43198  iunrelexp0  44486  uun123p4  45578  isosctrlem1ALT  45700  stoweidlem17  46789