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  9237  ltapr  11058  subadd  11488  ltaddsub  11716  leaddsub  11718  iooshf  13483  faclbnd4  14365  relexpsucl  15108  relexpsucr  15109  dvdsmulc  16379  lcmdvdsb  16709  infpnlem1  17008  fmf  24177  frgr3v  30763  nvs  31152  dipdi  31332  dipsubdi  31338  spansncol  32057  chirredlem2  32880  mdsymlem3  32894  isbasisrelowllem2  38118  ltflcei  38370  iscringd  38756  resubadd  43262  iunrelexp0  44550  uun123p4  45642  isosctrlem1ALT  45764  stoweidlem17  46853