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 1112	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3comr  1125  3coml  1127  oacan  8604  oaword1  8608  nnacan  8684  nnaword1  8685  elmapg  8897  fisseneq  9320  ltapr  11114  subadd  11539  ltaddsub  11764  leaddsub  11766  iooshf  13486  faclbnd4  14346  relexpsucl  15080  relexpsucr  15081  dvdsmulc  16332  lcmdvdsb  16660  infpnlem1  16957  fmf  23974  frgr3v  30307  nvs  30695  dipdi  30875  dipsubdi  30881  spansncol  31600  chirredlem2  32423  mdsymlem3  32437  isbasisrelowllem2  37322  ltflcei  37568  iscringd  37958  resubadd  42355  iunrelexp0  43664  uun123p4  44783  isosctrlem1ALT  44905  stoweidlem17  45938