Theorem 3com23 1209

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 1202	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1193	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3coml  1210  syld3an2  1285  3anidm13  1296  eqreu  2929  f1ofveu  5858  acexmid  5869  dfsmo2  6283  f1oeng  6752  ctssdc  7107  ltexprlemdisj  7600  ltexprlemfu  7605  recexprlemss1u  7630  mul32  8081  add32  8110  cnegexlem2  8127  subsub23  8156  subadd23  8163  addsub12  8164  subsub  8181  subsub3  8183  sub32  8185  suble  8391  lesub  8392  ltsub23  8393  ltsub13  8394  ltleadd  8397  div32ap  8643  div13ap  8644  div12ap  8645  divdiv32ap  8671  cju  8912  icc0r  9920  fzen  10036  elfz1b  10083  ioo0  10253  ico0  10255  ioc0  10256  expgt0  10546  expge0  10549  expge1  10550  shftval2  10826  abs3dif  11105  divalgb  11920  nnwodc  12027  ctinf  12421  grpinvcnv  12866  mulgaddcom  12934  mulgneg2  12944  srgrmhm  13077  ringcom  13114  mulgass2  13135  opprring  13148  unitmulcl  13181  restin  13458  cnpnei  13501  cnptoprest  13521  psmetsym  13611  xmetsym  13650