Theorem 3com23 1236

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3coml  1237  syld3an2  1321  3anidm13  1333  eqreu  3009  f1ofveu  6038  acexmid  6049  dfsmo2  6518  f1oeng  6996  ctssdc  7404  ltexprlemdisj  7921  ltexprlemfu  7926  recexprlemss1u  7951  mul32  8403  add32  8432  cnegexlem2  8449  subsub23  8478  subadd23  8485  addsub12  8486  subsub  8503  subsub3  8505  sub32  8507  suble  8714  lesub  8715  ltsub23  8716  ltsub13  8717  ltleadd  8720  div32ap  8966  div13ap  8967  div12ap  8968  divdiv32ap  8994  cju  9235  icc0r  10259  fzen  10377  elfz1b  10424  ioo0  10619  ico0  10621  ioc0  10622  expgt0  10934  expge0  10937  expge1  10938  shftval2  11511  abs3dif  11790  divalgb  12611  nnwodc  12732  ctinf  13181  grpinvcnv  13781  mulgaddcom  13863  mulgneg2  13873  srgrmhm  14138  ringcom  14175  mulgass2  14202  opprrng  14221  opprring  14223  unitmulcl  14258  islmodd  14441  lmodcom  14481  rmodislmod  14499  restin  15041  cnpnei  15084  cnptoprest  15104  psmetsym  15194  xmetsym  15233