Theorem 3com13 1123

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 1118	. 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  1124  3coml  1126  oacan  8585  oaword1  8589  nnacan  8665  nnaword1  8666  elmapg  8878  fisseneq  9291  ltapr  11083  subadd  11509  ltaddsub  11735  leaddsub  11737  iooshf  13463  faclbnd4  14333  relexpsucl  15067  relexpsucr  15068  dvdsmulc  16318  lcmdvdsb  16647  infpnlem1  16944  fmf  23969  frgr3v  30304  nvs  30692  dipdi  30872  dipsubdi  30878  spansncol  31597  chirredlem2  32420  mdsymlem3  32434  isbasisrelowllem2  37339  ltflcei  37595  iscringd  37985  resubadd  42386  iunrelexp0  43692  uun123p4  44810  isosctrlem1ALT  44932  stoweidlem17  45973