Theorem 3com13 1124

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 1119	. 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  1125  3coml  1127  oacan  8466  oaword1  8470  nnacan  8546  nnaword1  8547  elmapg  8766  fisseneq  9152  ltapr  10939  subadd  11366  ltaddsub  11594  leaddsub  11596  iooshf  13329  faclbnd4  14204  relexpsucl  14938  relexpsucr  14939  dvdsmulc  16194  lcmdvdsb  16524  infpnlem1  16822  fmf  23830  frgr3v  30219  nvs  30607  dipdi  30787  dipsubdi  30793  spansncol  31512  chirredlem2  32335  mdsymlem3  32349  isbasisrelowllem2  37330  ltflcei  37588  iscringd  37978  resubadd  42352  iunrelexp0  43675  uun123p4  44785  isosctrlem1ALT  44907  stoweidlem17  45998