Theorem 3com13 1123

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 1118	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3comr  1124  3coml  1126  oacan  8379  oaword1  8383  nnacan  8459  nnaword1  8460  elmapg  8628  fisseneq  9034  ltapr  10801  subadd  11224  ltaddsub  11449  leaddsub  11451  iooshf  13158  faclbnd4  14011  relexpsucl  14742  relexpsucr  14743  dvdsmulc  15993  lcmdvdsb  16318  infpnlem1  16611  fmf  23096  frgr3v  28639  nvs  29025  dipdi  29205  dipsubdi  29211  spansncol  29930  chirredlem2  30753  mdsymlem3  30767  isbasisrelowllem2  35527  ltflcei  35765  iscringd  36156  resubadd  40362  iunrelexp0  41310  uun123p4  42432  isosctrlem1ALT  42554  stoweidlem17  43558