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  5988  acexmid  5999  dfsmo2  6431  f1oeng  6906  ctssdc  7276  ltexprlemdisj  7789  ltexprlemfu  7794  recexprlemss1u  7819  mul32  8272  add32  8301  cnegexlem2  8318  subsub23  8347  subadd23  8354  addsub12  8355  subsub  8372  subsub3  8374  sub32  8376  suble  8583  lesub  8584  ltsub23  8585  ltsub13  8586  ltleadd  8589  div32ap  8835  div13ap  8836  div12ap  8837  divdiv32ap  8863  cju  9104  icc0r  10118  fzen  10235  elfz1b  10282  ioo0  10474  ico0  10476  ioc0  10477  expgt0  10789  expge0  10792  expge1  10793  shftval2  11332  abs3dif  11611  divalgb  12431  nnwodc  12552  ctinf  12996  grpinvcnv  13596  mulgaddcom  13678  mulgneg2  13688  srgrmhm  13952  ringcom  13989  mulgass2  14016  opprrng  14035  opprring  14037  unitmulcl  14071  islmodd  14251  lmodcom  14291  rmodislmod  14309  restin  14844  cnpnei  14887  cnptoprest  14907  psmetsym  14997  xmetsym  15036