Theorem 3com23 1191

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com23	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1184	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1176	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3coml  1192  syld3an2  1267  3anidm13  1278  eqreu  2904  f1ofveu  5812  acexmid  5823  dfsmo2  6234  f1oeng  6702  ctssdc  7057  ltexprlemdisj  7526  ltexprlemfu  7531  recexprlemss1u  7556  mul32  8005  add32  8034  cnegexlem2  8051  subsub23  8080  subadd23  8087  addsub12  8088  subsub  8105  subsub3  8107  sub32  8109  suble  8315  lesub  8316  ltsub23  8317  ltsub13  8318  ltleadd  8321  div32ap  8565  div13ap  8566  div12ap  8567  divdiv32ap  8593  cju  8832  icc0r  9830  fzen  9945  elfz1b  9992  ioo0  10159  ico0  10161  ioc0  10162  expgt0  10452  expge0  10455  expge1  10456  shftval2  10726  abs3dif  11005  divalgb  11816  ctinf  12170  restin  12587  cnpnei  12630  cnptoprest  12650  psmetsym  12740  xmetsym  12779