Theorem 3com13 1120

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3comr  1121  3coml  1123  oacan  8174  oaword1  8178  nnacan  8254  nnaword1  8255  elmapg  8419  fisseneq  8729  ltapr  10467  subadd  10889  ltaddsub  11114  leaddsub  11116  iooshf  12816  faclbnd4  13658  relexpsucr  14388  relexpsucl  14392  dvdsmulc  15637  lcmdvdsb  15957  infpnlem1  16246  fmf  22553  frgr3v  28054  nvs  28440  dipdi  28620  dipsubdi  28626  spansncol  29345  chirredlem2  30168  mdsymlem3  30182  isbasisrelowllem2  34640  ltflcei  34895  iscringd  35291  resubadd  39229  iunrelexp0  40067  uun123p4  41166  isosctrlem1ALT  41288  stoweidlem17  42322