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  7288  ltexprlemdisj  7801  ltexprlemfu  7806  recexprlemss1u  7831  mul32  8284  add32  8313  cnegexlem2  8330  subsub23  8359  subadd23  8366  addsub12  8367  subsub  8384  subsub3  8386  sub32  8388  suble  8595  lesub  8596  ltsub23  8597  ltsub13  8598  ltleadd  8601  div32ap  8847  div13ap  8848  div12ap  8849  divdiv32ap  8875  cju  9116  icc0r  10130  fzen  10247  elfz1b  10294  ioo0  10487  ico0  10489  ioc0  10490  expgt0  10802  expge0  10805  expge1  10806  shftval2  11345  abs3dif  11624  divalgb  12444  nnwodc  12565  ctinf  13009  grpinvcnv  13609  mulgaddcom  13691  mulgneg2  13701  srgrmhm  13965  ringcom  14002  mulgass2  14029  opprrng  14048  opprring  14050  unitmulcl  14085  islmodd  14265  lmodcom  14305  rmodislmod  14323  restin  14858  cnpnei  14901  cnptoprest  14921  psmetsym  15011  xmetsym  15050