Theorem 3com23 1209

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  3coml  1210  syld3an2  1285  3anidm13  1296  eqreu  2929  f1ofveu  5862  acexmid  5873  dfsmo2  6287  f1oeng  6756  ctssdc  7111  ltexprlemdisj  7604  ltexprlemfu  7609  recexprlemss1u  7634  mul32  8086  add32  8115  cnegexlem2  8132  subsub23  8161  subadd23  8168  addsub12  8169  subsub  8186  subsub3  8188  sub32  8190  suble  8396  lesub  8397  ltsub23  8398  ltsub13  8399  ltleadd  8402  div32ap  8648  div13ap  8649  div12ap  8650  divdiv32ap  8676  cju  8917  icc0r  9925  fzen  10042  elfz1b  10089  ioo0  10259  ico0  10261  ioc0  10262  expgt0  10552  expge0  10555  expge1  10556  shftval2  10834  abs3dif  11113  divalgb  11929  nnwodc  12036  ctinf  12430  grpinvcnv  12937  mulgaddcom  13005  mulgneg2  13015  srgrmhm  13175  ringcom  13212  mulgass2  13233  opprring  13247  unitmulcl  13280  islmodd  13381  restin  13646  cnpnei  13689  cnptoprest  13709  psmetsym  13799  xmetsym  13838