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  8560  oaword1  8564  nnacan  8640  nnaword1  8641  elmapg  8853  fisseneq  9265  ltapr  11059  subadd  11485  ltaddsub  11711  leaddsub  11713  iooshf  13443  faclbnd4  14315  relexpsucl  15050  relexpsucr  15051  dvdsmulc  16303  lcmdvdsb  16632  infpnlem1  16930  fmf  23883  frgr3v  30256  nvs  30644  dipdi  30824  dipsubdi  30830  spansncol  31549  chirredlem2  32372  mdsymlem3  32386  isbasisrelowllem2  37374  ltflcei  37632  iscringd  38022  resubadd  42422  iunrelexp0  43726  uun123p4  44836  isosctrlem1ALT  44958  stoweidlem17  46046