Theorem 3com23 1211

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1308  eqreu  2964  f1ofveu  5931  acexmid  5942  dfsmo2  6372  f1oeng  6847  ctssdc  7214  ltexprlemdisj  7718  ltexprlemfu  7723  recexprlemss1u  7748  mul32  8201  add32  8230  cnegexlem2  8247  subsub23  8276  subadd23  8283  addsub12  8284  subsub  8301  subsub3  8303  sub32  8305  suble  8512  lesub  8513  ltsub23  8514  ltsub13  8515  ltleadd  8518  div32ap  8764  div13ap  8765  div12ap  8766  divdiv32ap  8792  cju  9033  icc0r  10047  fzen  10164  elfz1b  10211  ioo0  10400  ico0  10402  ioc0  10403  expgt0  10715  expge0  10718  expge1  10719  shftval2  11108  abs3dif  11387  divalgb  12207  nnwodc  12328  ctinf  12772  grpinvcnv  13371  mulgaddcom  13453  mulgneg2  13463  srgrmhm  13727  ringcom  13764  mulgass2  13791  opprrng  13810  opprring  13812  unitmulcl  13846  islmodd  14026  lmodcom  14066  rmodislmod  14084  restin  14619  cnpnei  14662  cnptoprest  14682  psmetsym  14772  xmetsym  14811