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 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3comr  1143  3coml  1145  oacan  8529  oaword1  8533  nnacan  8610  nnaword1  8611  elmapg  8832  fisseneq  9219  ltapr  11025  subadd  11455  ltaddsub  11683  leaddsub  11685  iooshf  13448  faclbnd4  14329  relexpsucl  15064  relexpsucr  15065  dvdsmulc  16336  lcmdvdsb  16666  infpnlem1  16965  fmf  24102  frgr3v  30626  nvs  31015  dipdi  31195  dipsubdi  31201  spansncol  31920  chirredlem2  32743  mdsymlem3  32757  isbasisrelowllem2  38002  ltflcei  38259  iscringd  38649  resubadd  43140  iunrelexp0  44428  uun123p4  45520  isosctrlem1ALT  45642  stoweidlem17  46731