Theorem 3com13 1121

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3comr  1122  3coml  1124  oacan  8157  oaword1  8161  nnacan  8237  nnaword1  8238  elmapg  8402  fisseneq  8713  ltapr  10456  subadd  10878  ltaddsub  11103  leaddsub  11105  iooshf  12804  faclbnd4  13653  relexpsucl  14382  relexpsucr  14383  dvdsmulc  15629  lcmdvdsb  15947  infpnlem1  16236  fmf  22550  frgr3v  28060  nvs  28446  dipdi  28626  dipsubdi  28632  spansncol  29351  chirredlem2  30174  mdsymlem3  30188  isbasisrelowllem2  34773  ltflcei  35045  iscringd  35436  resubadd  39517  iunrelexp0  40403  uun123p4  41518  isosctrlem1ALT  41640  stoweidlem17  42659