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  8594  oaword1  8598  nnacan  8675  nnaword1  8676  elmapg  8897  fisseneq  9292  ltapr  11169  subadd  11599  ltaddsub  11830  leaddsub  11832  iooshf  13597  faclbnd4  14482  relexpsucl  15227  relexpsucr  15228  dvdsmulc  16497  lcmdvdsb  16832  infpnlem1  17132  fmf  24319  frgr3v  30933  nvs  31322  dipdi  31502  dipsubdi  31508  spansncol  32227  chirredlem2  33050  mdsymlem3  33064  isbasisrelowllem2  38547  ltflcei  38799  iscringd  39198  resubadd  43696  iunrelexp0  44963  uun123p4  46054  isosctrlem1ALT  46176  stoweidlem17  47300