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  8563  oaword1  8567  nnacan  8644  nnaword1  8645  elmapg  8866  fisseneq  9261  ltapr  11137  subadd  11567  ltaddsub  11797  leaddsub  11799  iooshf  13564  faclbnd4  14448  relexpsucl  15193  relexpsucr  15194  dvdsmulc  16462  lcmdvdsb  16797  infpnlem1  17097  fmf  24273  frgr3v  30885  nvs  31274  dipdi  31454  dipsubdi  31460  spansncol  32179  chirredlem2  33002  mdsymlem3  33016  isbasisrelowllem2  38388  ltflcei  38640  iscringd  39041  resubadd  43539  iunrelexp0  44811  uun123p4  45902  isosctrlem1ALT  46024  stoweidlem17  47135