Theorem 3com23 1233

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3coml  1234  syld3an2  1318  3anidm13  1330  eqreu  2996  f1ofveu  6001  acexmid  6012  dfsmo2  6448  f1oeng  6925  ctssdc  7303  ltexprlemdisj  7816  ltexprlemfu  7821  recexprlemss1u  7846  mul32  8299  add32  8328  cnegexlem2  8345  subsub23  8374  subadd23  8381  addsub12  8382  subsub  8399  subsub3  8401  sub32  8403  suble  8610  lesub  8611  ltsub23  8612  ltsub13  8613  ltleadd  8616  div32ap  8862  div13ap  8863  div12ap  8864  divdiv32ap  8890  cju  9131  icc0r  10151  fzen  10268  elfz1b  10315  ioo0  10509  ico0  10511  ioc0  10512  expgt0  10824  expge0  10827  expge1  10828  shftval2  11377  abs3dif  11656  divalgb  12476  nnwodc  12597  ctinf  13041  grpinvcnv  13641  mulgaddcom  13723  mulgneg2  13733  srgrmhm  13997  ringcom  14034  mulgass2  14061  opprrng  14080  opprring  14082  unitmulcl  14117  islmodd  14297  lmodcom  14337  rmodislmod  14355  restin  14890  cnpnei  14933  cnptoprest  14953  psmetsym  15043  xmetsym  15082