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 1112	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3comr  1126  3coml  1128  oacan  8485  oaword1  8489  nnacan  8566  nnaword1  8567  elmapg  8788  fisseneq  9175  ltapr  10968  subadd  11395  ltaddsub  11623  leaddsub  11625  iooshf  13354  faclbnd4  14232  relexpsucl  14966  relexpsucr  14967  dvdsmulc  16222  lcmdvdsb  16552  infpnlem1  16850  fmf  23901  frgr3v  30362  nvs  30751  dipdi  30931  dipsubdi  30937  spansncol  31656  chirredlem2  32479  mdsymlem3  32493  isbasisrelowllem2  37611  ltflcei  37859  iscringd  38249  resubadd  42749  iunrelexp0  44058  uun123p4  45167  isosctrlem1ALT  45289  stoweidlem17  46375