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  2930  f1ofveu  5863  acexmid  5874  dfsmo2  6288  f1oeng  6757  ctssdc  7112  ltexprlemdisj  7605  ltexprlemfu  7610  recexprlemss1u  7635  mul32  8087  add32  8116  cnegexlem2  8133  subsub23  8162  subadd23  8169  addsub12  8170  subsub  8187  subsub3  8189  sub32  8191  suble  8397  lesub  8398  ltsub23  8399  ltsub13  8400  ltleadd  8403  div32ap  8649  div13ap  8650  div12ap  8651  divdiv32ap  8677  cju  8918  icc0r  9926  fzen  10043  elfz1b  10090  ioo0  10260  ico0  10262  ioc0  10263  expgt0  10553  expge0  10556  expge1  10557  shftval2  10835  abs3dif  11114  divalgb  11930  nnwodc  12037  ctinf  12431  grpinvcnv  12938  mulgaddcom  13007  mulgneg2  13017  srgrmhm  13177  ringcom  13214  mulgass2  13235  opprring  13249  unitmulcl  13282  islmodd  13383  lmodcom  13423  rmodislmod  13441  restin  13679  cnpnei  13722  cnptoprest  13742  psmetsym  13832  xmetsym  13871