Theorem 3com13 1140

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3comr  1141  3coml  1143  oacan  8532  oaword1  8536  nnacan  8613  nnaword1  8614  elmapg  8835  fisseneq  9222  ltapr  11029  subadd  11459  ltaddsub  11687  leaddsub  11689  iooshf  13452  faclbnd4  14332  relexpsucl  15067  relexpsucr  15068  dvdsmulc  16340  lcmdvdsb  16670  infpnlem1  16969  fmf  24070  frgr3v  30566  nvs  30955  dipdi  31135  dipsubdi  31141  spansncol  31860  chirredlem2  32683  mdsymlem3  32697  isbasisrelowllem2  37889  ltflcei  38146  iscringd  38536  resubadd  43029  iunrelexp0  44319  uun123p4  45411  isosctrlem1ALT  45533  stoweidlem17  46622