Theorem 3com13 1142

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3coml  1145  oacan  8535  oaword1  8539  nnacan  8616  nnaword1  8617  elmapg  8838  fisseneq  9233  ltapr  11054  subadd  11484  ltaddsub  11712  leaddsub  11714  iooshf  13479  faclbnd4  14361  relexpsucl  15104  relexpsucr  15105  dvdsmulc  16373  lcmdvdsb  16703  infpnlem1  17002  fmf  24171  frgr3v  30755  nvs  31144  dipdi  31324  dipsubdi  31330  spansncol  32049  chirredlem2  32872  mdsymlem3  32886  isbasisrelowllem2  38110  ltflcei  38362  iscringd  38748  resubadd  43254  iunrelexp0  44542  uun123p4  45634  isosctrlem1ALT  45756  stoweidlem17  46845