Theorem 3com13 1125

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3comr  1126  3coml  1128  oacan  8548  oaword1  8552  nnacan  8628  nnaword1  8629  elmapg  8833  fisseneq  9257  ltapr  11040  subadd  11463  ltaddsub  11688  leaddsub  11690  iooshf  13403  faclbnd4  14257  relexpsucl  14978  relexpsucr  14979  dvdsmulc  16227  lcmdvdsb  16550  infpnlem1  16843  fmf  23449  frgr3v  29528  nvs  29916  dipdi  30096  dipsubdi  30102  spansncol  30821  chirredlem2  31644  mdsymlem3  31658  isbasisrelowllem2  36237  ltflcei  36476  iscringd  36866  resubadd  41252  iunrelexp0  42453  uun123p4  43573  isosctrlem1ALT  43695  stoweidlem17  44733