Theorem 3com13 1158

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  3comr  1159  3coml  1161  3adant3lOLD  1234  3adant3rOLD  1236  syld3an1OLD  1534  oacan  7895  oaword1  7899  nnacan  7975  nnaword1  7976  elmapg  8135  fisseneq  8440  ltapr  10182  subadd  10604  ltaddsub  10826  leaddsub  10828  iooshf  12540  faclbnd4  13377  relexpsucr  14146  relexpsucl  14150  dvdsmulc  15386  lcmdvdsb  15699  infpnlem1  15985  fmf  22119  frgr3v  27645  nvs  28062  dipdi  28242  dipsubdi  28248  spansncol  28971  chirredlem2  29794  mdsymlem3  29808  isbasisrelowllem2  33742  ltflcei  33933  iscringd  34332  resubadd  38077  iunrelexp0  38828  uun123p4  39859  isosctrlem1ALT  39981  stoweidlem17  41021