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  8477  oaword1  8481  nnacan  8558  nnaword1  8559  elmapg  8780  fisseneq  9167  ltapr  10960  subadd  11387  ltaddsub  11615  leaddsub  11617  iooshf  13346  faclbnd4  14224  relexpsucl  14958  relexpsucr  14959  dvdsmulc  16214  lcmdvdsb  16544  infpnlem1  16842  fmf  23893  frgr3v  30333  nvs  30721  dipdi  30901  dipsubdi  30907  spansncol  31626  chirredlem2  32449  mdsymlem3  32463  isbasisrelowllem2  37532  ltflcei  37780  iscringd  38170  resubadd  42670  iunrelexp0  43979  uun123p4  45088  isosctrlem1ALT  45210  stoweidlem17  46297