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  8549  oaword1  8553  nnacan  8630  nnaword1  8631  elmapg  8852  fisseneq  9247  ltapr  11123  subadd  11553  ltaddsub  11783  leaddsub  11785  iooshf  13550  faclbnd4  14434  relexpsucl  15177  relexpsucr  15178  dvdsmulc  16446  lcmdvdsb  16781  infpnlem1  17081  fmf  24257  frgr3v  30869  nvs  31258  dipdi  31438  dipsubdi  31444  spansncol  32163  chirredlem2  32986  mdsymlem3  33000  isbasisrelowllem2  38259  ltflcei  38511  iscringd  38912  resubadd  43410  iunrelexp0  44687  uun123p4  45779  isosctrlem1ALT  45901  stoweidlem17  46996