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  8512  oaword1  8516  nnacan  8592  nnaword1  8593  elmapg  8812  fisseneq  9204  ltapr  10998  subadd  11424  ltaddsub  11652  leaddsub  11654  iooshf  13387  faclbnd4  14262  relexpsucl  14997  relexpsucr  14998  dvdsmulc  16253  lcmdvdsb  16583  infpnlem1  16881  fmf  23832  frgr3v  30204  nvs  30592  dipdi  30772  dipsubdi  30778  spansncol  31497  chirredlem2  32320  mdsymlem3  32334  isbasisrelowllem2  37344  ltflcei  37602  iscringd  37992  resubadd  42367  iunrelexp0  43691  uun123p4  44801  isosctrlem1ALT  44923  stoweidlem17  46015