Theorem 3com23 1187

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

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3coml  1188  syld3an2  1263  3anidm13  1274  eqreu  2876  f1ofveu  5762  acexmid  5773  dfsmo2  6184  f1oeng  6651  ctssdc  6998  ltexprlemdisj  7414  ltexprlemfu  7419  recexprlemss1u  7444  mul32  7892  add32  7921  cnegexlem2  7938  subsub23  7967  subadd23  7974  addsub12  7975  subsub  7992  subsub3  7994  sub32  7996  suble  8202  lesub  8203  ltsub23  8204  ltsub13  8205  ltleadd  8208  div32ap  8452  div13ap  8453  div12ap  8454  divdiv32ap  8480  cju  8719  icc0r  9709  fzen  9823  elfz1b  9870  ioo0  10037  ico0  10039  ioc0  10040  expgt0  10326  expge0  10329  expge1  10330  shftval2  10598  abs3dif  10877  divalgb  11622  ctinf  11943  restin  12345  cnpnei  12388  cnptoprest  12408  psmetsym  12498  xmetsym  12537