Theorem 3com13 1122

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

Syntax hints:   → wi 4   ∧ w3a 1085

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

This theorem is referenced by:  3comr  1123  3coml  1125  oacan  8341  oaword1  8345  nnacan  8421  nnaword1  8422  elmapg  8586  fisseneq  8963  ltapr  10732  subadd  11154  ltaddsub  11379  leaddsub  11381  iooshf  13087  faclbnd4  13939  relexpsucl  14670  relexpsucr  14671  dvdsmulc  15921  lcmdvdsb  16246  infpnlem1  16539  fmf  23004  frgr3v  28540  nvs  28926  dipdi  29106  dipsubdi  29112  spansncol  29831  chirredlem2  30654  mdsymlem3  30668  isbasisrelowllem2  35454  ltflcei  35692  iscringd  36083  resubadd  40283  iunrelexp0  41199  uun123p4  42321  isosctrlem1ALT  42443  stoweidlem17  43448