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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3comr  1125  3coml  1127  oacan  8547  oaword1  8551  nnacan  8627  nnaword1  8628  elmapg  8832  fisseneq  9256  ltapr  11039  subadd  11462  ltaddsub  11687  leaddsub  11689  iooshf  13402  faclbnd4  14256  relexpsucl  14977  relexpsucr  14978  dvdsmulc  16226  lcmdvdsb  16549  infpnlem1  16842  fmf  23448  frgr3v  29525  nvs  29911  dipdi  30091  dipsubdi  30097  spansncol  30816  chirredlem2  31639  mdsymlem3  31653  isbasisrelowllem2  36232  ltflcei  36471  iscringd  36861  resubadd  41253  iunrelexp0  42443  uun123p4  43563  isosctrlem1ALT  43685  stoweidlem17  44723