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  2999  f1ofveu  6016  acexmid  6027  dfsmo2  6496  f1oeng  6973  ctssdc  7355  ltexprlemdisj  7869  ltexprlemfu  7874  recexprlemss1u  7899  mul32  8351  add32  8380  cnegexlem2  8397  subsub23  8426  subadd23  8433  addsub12  8434  subsub  8451  subsub3  8453  sub32  8455  suble  8662  lesub  8663  ltsub23  8664  ltsub13  8665  ltleadd  8668  div32ap  8914  div13ap  8915  div12ap  8916  divdiv32ap  8942  cju  9183  icc0r  10205  fzen  10323  elfz1b  10370  ioo0  10565  ico0  10567  ioc0  10568  expgt0  10880  expge0  10883  expge1  10884  shftval2  11449  abs3dif  11728  divalgb  12549  nnwodc  12670  ctinf  13114  grpinvcnv  13714  mulgaddcom  13796  mulgneg2  13806  srgrmhm  14071  ringcom  14108  mulgass2  14135  opprrng  14154  opprring  14156  unitmulcl  14191  islmodd  14372  lmodcom  14412  rmodislmod  14430  restin  14970  cnpnei  15013  cnptoprest  15033  psmetsym  15123  xmetsym  15162