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  11079  abs3dif  11358  divalgb  12178  nnwodc  12299  ctinf  12743  grpinvcnv  13342  mulgaddcom  13424  mulgneg2  13434  srgrmhm  13698  ringcom  13735  mulgass2  13762  opprrng  13781  opprring  13783  unitmulcl  13817  islmodd  13997  lmodcom  14037  rmodislmod  14055  restin  14590  cnpnei  14633  cnptoprest  14653  psmetsym  14743  xmetsym  14782