Theorem 3com13 1125

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 1120	. 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  1126  3coml  1128  oacan  8483  oaword1  8487  nnacan  8564  nnaword1  8565  elmapg  8786  fisseneq  9173  ltapr  10968  subadd  11396  ltaddsub  11624  leaddsub  11626  iooshf  13379  faclbnd4  14259  relexpsucl  14993  relexpsucr  14994  dvdsmulc  16252  lcmdvdsb  16582  infpnlem1  16881  fmf  23910  frgr3v  30345  nvs  30734  dipdi  30914  dipsubdi  30920  spansncol  31639  chirredlem2  32462  mdsymlem3  32476  isbasisrelowllem2  37672  ltflcei  37929  iscringd  38319  resubadd  42811  iunrelexp0  44129  uun123p4  45238  isosctrlem1ALT  45360  stoweidlem17  46445