Theorem 3com23 1211

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1307  eqreu  2956  f1ofveu  5913  acexmid  5924  dfsmo2  6354  f1oeng  6825  ctssdc  7188  ltexprlemdisj  7692  ltexprlemfu  7697  recexprlemss1u  7722  mul32  8175  add32  8204  cnegexlem2  8221  subsub23  8250  subadd23  8257  addsub12  8258  subsub  8275  subsub3  8277  sub32  8279  suble  8486  lesub  8487  ltsub23  8488  ltsub13  8489  ltleadd  8492  div32ap  8738  div13ap  8739  div12ap  8740  divdiv32ap  8766  cju  9007  icc0r  10020  fzen  10137  elfz1b  10184  ioo0  10368  ico0  10370  ioc0  10371  expgt0  10683  expge0  10686  expge1  10687  shftval2  11010  abs3dif  11289  divalgb  12109  nnwodc  12230  ctinf  12674  grpinvcnv  13272  mulgaddcom  13354  mulgneg2  13364  srgrmhm  13628  ringcom  13665  mulgass2  13692  opprrng  13711  opprring  13713  unitmulcl  13747  islmodd  13927  lmodcom  13967  rmodislmod  13985  restin  14520  cnpnei  14563  cnptoprest  14583  psmetsym  14673  xmetsym  14712