Theorem 3com23 1233

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3coml  1234  syld3an2  1318  3anidm13  1330  eqreu  2995  f1ofveu  5995  acexmid  6006  dfsmo2  6439  f1oeng  6916  ctssdc  7291  ltexprlemdisj  7804  ltexprlemfu  7809  recexprlemss1u  7834  mul32  8287  add32  8316  cnegexlem2  8333  subsub23  8362  subadd23  8369  addsub12  8370  subsub  8387  subsub3  8389  sub32  8391  suble  8598  lesub  8599  ltsub23  8600  ltsub13  8601  ltleadd  8604  div32ap  8850  div13ap  8851  div12ap  8852  divdiv32ap  8878  cju  9119  icc0r  10134  fzen  10251  elfz1b  10298  ioo0  10491  ico0  10493  ioc0  10494  expgt0  10806  expge0  10809  expge1  10810  shftval2  11352  abs3dif  11631  divalgb  12451  nnwodc  12572  ctinf  13016  grpinvcnv  13616  mulgaddcom  13698  mulgneg2  13708  srgrmhm  13972  ringcom  14009  mulgass2  14036  opprrng  14055  opprring  14057  unitmulcl  14092  islmodd  14272  lmodcom  14312  rmodislmod  14330  restin  14865  cnpnei  14908  cnptoprest  14928  psmetsym  15018  xmetsym  15057