Theorem 3com13 1124

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3comr  1125  3coml  1127  oacan  8463  oaword1  8467  nnacan  8543  nnaword1  8544  elmapg  8763  fisseneq  9147  ltapr  10936  subadd  11363  ltaddsub  11591  leaddsub  11593  iooshf  13326  faclbnd4  14204  relexpsucl  14938  relexpsucr  14939  dvdsmulc  16194  lcmdvdsb  16524  infpnlem1  16822  fmf  23860  frgr3v  30255  nvs  30643  dipdi  30823  dipsubdi  30829  spansncol  31548  chirredlem2  32371  mdsymlem3  32385  isbasisrelowllem2  37398  ltflcei  37656  iscringd  38046  resubadd  42420  iunrelexp0  43743  uun123p4  44852  isosctrlem1ALT  44974  stoweidlem17  46063