Theorem 3com23 1212

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  3coml  1213  syld3an2  1297  3anidm13  1309  eqreu  2969  f1ofveu  5945  acexmid  5956  dfsmo2  6386  f1oeng  6861  ctssdc  7230  ltexprlemdisj  7739  ltexprlemfu  7744  recexprlemss1u  7769  mul32  8222  add32  8251  cnegexlem2  8268  subsub23  8297  subadd23  8304  addsub12  8305  subsub  8322  subsub3  8324  sub32  8326  suble  8533  lesub  8534  ltsub23  8535  ltsub13  8536  ltleadd  8539  div32ap  8785  div13ap  8786  div12ap  8787  divdiv32ap  8813  cju  9054  icc0r  10068  fzen  10185  elfz1b  10232  ioo0  10424  ico0  10426  ioc0  10427  expgt0  10739  expge0  10742  expge1  10743  shftval2  11212  abs3dif  11491  divalgb  12311  nnwodc  12432  ctinf  12876  grpinvcnv  13475  mulgaddcom  13557  mulgneg2  13567  srgrmhm  13831  ringcom  13868  mulgass2  13895  opprrng  13914  opprring  13916  unitmulcl  13950  islmodd  14130  lmodcom  14170  rmodislmod  14188  restin  14723  cnpnei  14766  cnptoprest  14786  psmetsym  14876  xmetsym  14915