Theorem 3com23 1152

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

Syntax hints:   → wi 4   ∧ w3a 927

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

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

This theorem is referenced by:  3coml  1153  syld3an2  1228  3anidm13  1239  eqreu  2821  f1ofveu  5678  acexmid  5689  dfsmo2  6090  f1oeng  6554  ltexprlemdisj  7262  ltexprlemfu  7267  recexprlemss1u  7292  mul32  7709  add32  7738  cnegexlem2  7755  subsub23  7784  subadd23  7791  addsub12  7792  subsub  7809  subsub3  7811  sub32  7813  suble  8015  lesub  8016  ltsub23  8017  ltsub13  8018  ltleadd  8021  div32ap  8256  div13ap  8257  div12ap  8258  divdiv32ap  8284  cju  8519  icc0r  9492  fzen  9606  elfz1b  9653  ioo0  9820  ico0  9822  ioc0  9823  expgt0  10103  expge0  10106  expge1  10107  shftval2  10375  abs3dif  10653  divalgb  11352  restin  12028  cnpnei  12070  cnptoprest  12090  psmetsym  12115  xmetsym  12154