Theorem 3com13 1137

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 1132	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp31 1124	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3comr  1138  3coml  1140  oacan  8517  oaword1  8521  nnacan  8598  nnaword1  8599  elmapg  8820  fisseneq  9207  ltapr  11003  subadd  11433  ltaddsub  11661  leaddsub  11663  iooshf  13430  faclbnd4  14310  relexpsucl  15044  relexpsucr  15045  dvdsmulc  16317  lcmdvdsb  16647  infpnlem1  16946  fmf  24002  frgr3v  30474  nvs  30863  dipdi  31043  dipsubdi  31049  spansncol  31768  chirredlem2  32591  mdsymlem3  32605  isbasisrelowllem2  37847  ltflcei  38104  iscringd  38494  resubadd  42985  iunrelexp0  44275  uun123p4  45384  isosctrlem1ALT  45506  stoweidlem17  46588